Theorem Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply

Modification history

2024-03-05 14:11

Mathlib/RingTheory/Ideal/QuotientOperations.lean

chore: fix simp issues around Ideal.quotientKerAlgEquivOfRightInverse (#11014) …

Deleted Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply View on Github →

2023-04-05 08:46

Mathlib/RingTheory/Ideal/QuotientOperations.lean

feat: port RingTheory.Ideal.QuotientOperations (#2757) …

Added Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply View on Github →