Theorem Ideal.ker_quotientMap_mk

Modification history

2025-02-04 15:13

Mathlib/RingTheory/Ideal/Quotient/Operations.lean

refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930)

Modified Ideal.ker_quotientMap_mk View on Github →

2024-10-17 14:30

Mathlib/RingTheory/Ideal/QuotientOperations.lean

feat(RingTheory/Smooth): Smoothness of product rings. (#15131)

Added Ideal.ker_quotientMap_mk View on Github →