Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 04:11 8a2d93a0

View on Github →

feat(ring_theory/etale): Localization and formally etale homomorphisms. (#15813)

Estimated changes

Modified src/ring_theory/etale.lean

added theorem algebra.formally_etale.localization_base

added theorem algebra.formally_etale.localization_map

added theorem algebra.formally_etale.of_is_localization

added theorem algebra.formally_smooth.localization_base

added theorem algebra.formally_smooth.localization_map

added theorem algebra.formally_smooth.of_is_localization

added theorem algebra.formally_unramified.localization_base

added theorem algebra.formally_unramified.localization_map

added theorem algebra.formally_unramified.of_comp

added theorem algebra.formally_unramified.of_is_localization

Modified src/ring_theory/nilpotent.lean

modified theorem ideal.is_nilpotent.induction_on

added theorem is_nilpotent.is_unit_quotient_mk_iff