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