Theorem Algebra.Extension.Algebra.FormallySmooth.iff_of_surjective

Modification history

2025-11-17 16:19
Mathlib/RingTheory/Smooth/Basic.lean
feat(RingTheory): miscellaneous lemmas about etale (#30857)
Added Algebra.Extension.Algebra.FormallySmooth.iff_of_surjectiveView on Github →