Theorem coe_subset_nonunits

Modification history

2024-11-14 19:40

Mathlib/RingTheory/Ideal/Basic.lean

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

Modified coe_subset_nonunits View on Github →

2023-02-21 09:05

Mathlib/RingTheory/Ideal/Basic.lean

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

Added coe_subset_nonunits View on Github →