Mathlib Changelog
Changelog
About
Github
Commit
2022-07-20 07:41
ffc640f4
View on Github →
feat(ring_theory/derivation): Derivations into square-zero ideals corresponds to liftings. (
#15244
)
Estimated changes
Modified
src/ring_theory/derivation.lean
added
def
derivation_to_square_zero_equiv_lift
added
def
derivation_to_square_zero_of_lift
added
theorem
derivation_to_square_zero_of_lift_apply
added
def
diff_to_ideal_of_quotient_comp_eq
added
theorem
diff_to_ideal_of_quotient_comp_eq_apply
added
def
lift_of_derivation_to_square_zero
added
theorem
lift_of_derivation_to_square_zero_apply
added
theorem
lift_of_derivation_to_square_zero_mk_apply