mem_nonunits_iff_exists_mem_maximalIdeal

English

An element a ∈ K lies in A.nonunits iff there exists ha ∈ A with ⟨a, ha⟩ in the maximal ideal of A.

Русский

Элемент a ∈ K принадлежит A.nonunits тогда и только тогда, когда существует ha ∈ A such that ⟨a, ha⟩ принадлежит максимальной идеалу A.

LaTeX

$$$a \in A_{\mathrm{nonunits}} \iff \exists ha, \ (\langle a, ha \rangle : A) \in \mathrm{IsLocalRing.maximalIdeal}(A)$$$

Lean4

/-- The elements of `A.nonunits` are those of the maximal ideal of `A`.

See also `coe_mem_nonunits_iff`, which has a simpler right-hand side but requires the element
to be in `A` already.
-/
theorem mem_nonunits_iff_exists_mem_maximalIdeal {a : K} :
    a ∈ A.nonunits ↔ ∃ ha, (⟨a, ha⟩ : A) ∈ IsLocalRing.maximalIdeal A :=
  ⟨fun h => ⟨nonunits_subset h, coe_mem_nonunits_iff.mp h⟩, fun ⟨_, h⟩ => coe_mem_nonunits_iff.mpr h⟩

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