valuation_lt_one_iff — Mathlib

English

An element a ∈ A lies in the maximal ideal of A iff A.valuation(a) < 1.

Русский

Элемент a ∈ A лежит в максимальном идеале A тогда и только тогда, когда A.valuation(a) < 1.

LaTeX

$$$a\in \mathrm{IsLocalRing.maximalIdeal}(A) \iff A.valuation(a) < 1$$$

Lean4

theorem valuation_lt_one_iff (a : A) : a ∈ IsLocalRing.maximalIdeal A ↔ A.valuation a < 1 :=
  by
  rw [IsLocalRing.mem_maximalIdeal]
  dsimp [nonunits]; rw [valuation_eq_one_iff]
  exact (A.valuation_le_one a).lt_iff_ne.symm

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