coe_subset_nonunits — Mathlib

English

If a proper ideal I ≠ ⊤ in a semiring, then its underlying set lies inside the nonunits.

Русский

Если идеал I ≠ ⊤ в полугруппе, то множество элементов I состоит из неединиц.

LaTeX

$$I ≠ ⊤ \Rightarrow (I : \mathrm{Set}\ α) \subseteq nonunits(α)$$

Lean4

theorem coe_subset_nonunits [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : (I : Set α) ⊆ nonunits α := fun _x hx hu =>
  h <| I.eq_top_of_isUnit_mem hx hu

Похожие утверждения