Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-18 09:39 eba35e3a

View on Github →

feat(ring_theory/etale): Condition for a quotient of a formally smooth algebra to be formally smooth. (#15842)

Estimated changes

Modified src/ring_theory/etale.lean

added theorem algebra.formally_smooth.comp_lift_of_surjective

added theorem algebra.formally_smooth.iff_split_surjection

added def algebra.formally_smooth.lift_of_surjective

added theorem algebra.formally_smooth.lift_of_surjective_apply

added theorem algebra.formally_smooth.of_split

Modified src/ring_theory/ideal/cotangent.lean

added theorem alg_hom.ker_ker_sqare_lift

added def alg_hom.ker_square_lift

added theorem ideal.cotangent_ideal_square

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.le_comap_pow

added theorem ideal.pow_mono

added def ideal.quotient.liftₐ

added theorem ideal.quotient.liftₐ_apply

added theorem ideal.quotient.liftₐ_comp