Theorem exists_max_ideal_of_mem_nonunits

Modification history

2024-11-14 19:40

Mathlib/RingTheory/Ideal/Basic.lean

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

Modified exists_max_ideal_of_mem_nonunits View on Github →

2023-02-21 09:05

Mathlib/RingTheory/Ideal/Basic.lean

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

Added exists_max_ideal_of_mem_nonunits View on Github →