feat(RingTheory/Smooth): formally smooth iff H¹(L_{R/S}) = 0
and Ω_{S/R}
is projective
#62534
add_label_from_comment.yml
on: issue_comment
Add ready-to-merge label
0s
Add delegated label
0s