Commit 2023-06-03 07:38 e611ab98

View on Github →

feat: port RingTheory.Derivation.ToSquareZero (#4614)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Derivation/ToSquareZero.lean

added def derivationToSquareZeroEquivLift

added def derivationToSquareZeroOfLift

added theorem derivationToSquareZeroOfLift_apply

added def diffToIdealOfQuotientCompEq

added theorem diffToIdealOfQuotientCompEq_apply

added def liftOfDerivationToSquareZero

added theorem liftOfDerivationToSquareZero_mk_apply'

added theorem liftOfDerivationToSquareZero_mk_apply