image_maximalIdeal — Mathlib

English

The image of the maximal ideal of A in K equals A.nonunits.

Русский

Образ максимальной идеалы A в K равен A.nonunits.

LaTeX

$$$\big( (\uparrow) : A \to K \big)'' \mathrm{IsLocalRing.maximalIdeal} (A) = A_{\mathrm{nonunits}}$$$

Lean4

/-- `A.nonunits` agrees with the maximal ideal of `A`, after taking its image in `K`. -/
theorem image_maximalIdeal : ((↑) : A → K) '' IsLocalRing.maximalIdeal A = A.nonunits :=
  by
  ext a
  simp only [Set.mem_image, SetLike.mem_coe, mem_nonunits_iff_exists_mem_maximalIdeal]
  rw [Subtype.exists]
  simp_rw [exists_and_right, exists_eq_right]

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