Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-07-19 11:15
1b775c2c
View on Github →
feat(ring_theory/etale): Formally étale morphisms. (
#15242
)
Estimated changes
Created
src/ring_theory/etale.lean
added
theorem
algebra.formally_etale.comp
added
theorem
algebra.formally_etale.iff_unramified_and_smooth
added
theorem
algebra.formally_etale.of_equiv
added
theorem
algebra.formally_etale.of_unramified_and_smooth
added
theorem
algebra.formally_smooth.comp
added
theorem
algebra.formally_smooth.comp_lift
added
theorem
algebra.formally_smooth.exists_lift
added
def
algebra.formally_smooth.lift
added
theorem
algebra.formally_smooth.mk_lift
added
theorem
algebra.formally_smooth.of_equiv
added
theorem
algebra.formally_unramified.comp
added
theorem
algebra.formally_unramified.ext
added
theorem
algebra.formally_unramified.lift_unique
added
theorem
algebra.formally_unramified.of_equiv
Modified
src/ring_theory/nilpotent.lean
added
theorem
ideal.is_nilpotent.induction_on