Theorem Ideal.ker_quotient_lift

Modification history

2024-01-08 12:05

Mathlib/RingTheory/Ideal/QuotientOperations.lean

feat (RingTheory/Ideal/QuotientOperations) : remove commutativity assumption (#9495) …

Modified Ideal.ker_quotient_lift View on Github →

2023-04-05 08:46

Mathlib/RingTheory/Ideal/QuotientOperations.lean

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

Added Ideal.ker_quotient_lift View on Github →