Commit 2024-03-05 14:11 c84996b8

View on Github →

chore: fix simp issues around Ideal.quotientKerAlgEquivOfRightInverse (#11014) Several simp lemmas were poorly named and not in simp normal form.

Estimated changes

Modified Mathlib/RingTheory/Etale.lean

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

modified theorem Ideal.KerLift.map_smul

deleted theorem Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply

modified def Ideal.kerLiftAlg

deleted theorem Ideal.quotientKerAlgEquivOfRightInverse.apply