Theorem Ideal.Quotient.zero_ne_one_iff

Modification history

2025-02-04 15:13

Mathlib/RingTheory/Ideal/Quotient/Basic.lean

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

Modified Ideal.Quotient.zero_ne_one_iff View on Github →

2023-03-09 08:47

Mathlib/RingTheory/Ideal/Quotient.lean

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

Added Ideal.Quotient.zero_ne_one_iff View on Github →