Commit 2023-05-29 12:31 63c05ba6

View on Github →

feat: port RingTheory.Ideal.Cotangent (#4451)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Cotangent.lean

added def AlgHom.kerSquareLift

added theorem AlgHom.ker_ker_sqare_lift

added def Ideal.Cotangent

added theorem Ideal.cotangentEquivIdeal_apply

added theorem Ideal.cotangentEquivIdeal_symm_apply

added def Ideal.cotangentIdeal

added theorem Ideal.cotangentIdeal_square

added def Ideal.cotangentToQuotientSquare

added theorem Ideal.cotangent_subsingleton_iff

added theorem Ideal.map_toCotangent_ker

added theorem Ideal.mem_toCotangent_ker

added def Ideal.quotCotangent

added def Ideal.toCotangent

added theorem Ideal.toCotangent_eq

added theorem Ideal.toCotangent_eq_zero

added theorem Ideal.toCotangent_range

added theorem Ideal.toCotangent_surjective

added theorem Ideal.toCotangent_to_quotient_square

added theorem Ideal.to_quotient_square_comp_toCotangent

added theorem Ideal.to_quotient_square_range

added def LocalRing.CotangentSpace