Def Ideal.Quotient.factor

Modification history

2024-10-30 08:00

Mathlib/RingTheory/Ideal/Quotient/Basic.lean

chore(RingTheory/Ideal): split `Quotient.lean` into `Defs` and `Basic` (#18393) …

Modified Ideal.Quotient.factor View on Github →

2023-03-09 08:47

Mathlib/RingTheory/Ideal/Quotient.lean

feat: port RingTheory.Ideal.Quotient (#2412)

Added Ideal.Quotient.factor View on Github →