coe_mem_nonunits_iff — Mathlib

English

For a ∈ ValuationSubring K, (a : K) ∈ A.nonunits iff a ∈ IsLocalRing.maximalIdeal A after appropriate coercion.

Русский

Для a ∈ A, образ a в K принадлежит A.nonunits тогда и только тогда, когда через подходящее приведение a принадлежит максимальной идеалу A.

LaTeX

$$$(a : K) \in A_{\mathrm{nonunits}} \iff a \in \mathrm{IsLocalRing.maximalIdeal}(A)$$$

Lean4

/-- The elements of `A.nonunits` are those of the maximal ideal of `A` after coercion to `K`.

See also `mem_nonunits_iff_exists_mem_maximalIdeal`, which gets rid of the coercion to `K`,
at the expense of a more complicated right-hand side.
-/
theorem coe_mem_nonunits_iff {a : A} : (a : K) ∈ A.nonunits ↔ a ∈ IsLocalRing.maximalIdeal A :=
  (valuation_lt_one_iff _ _).symm

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