Theorem one_not_mem_nonunits

Modification history

2024-11-14 19:40

Mathlib/RingTheory/Ideal/Basic.lean

chore(RingTheory/Ideal): split off material on `nonunits` (#19035) …

Modified one_not_mem_nonunits View on Github →

2023-02-21 09:05

Mathlib/RingTheory/Ideal/Basic.lean

feat: port RingTheory.Ideal.Basic (#2283) …

Added one_not_mem_nonunits View on Github →