Mathlib v3 is deprecated. Go to Mathlib v4

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