mem_integer_iff — Mathlib

English

For every x in K, x lies in the integer part of the valuation iff x equals algebraMap(A,K,a) for some a in A.

Русский

Для каждого элемента x в K верно: x принадлежит диапазону целого (integer) в оценке тогда и только тогда, когда существует a ∈ A такое, что x = algebraMap A K a.

LaTeX

$$$ x \\in (\\mathrm{valuation} A K).\\mathrm{integer} \\iff \\exists a \\in A, \\ \\mathrm{algebraMap} A K\\ a = x $$$

Lean4

theorem mem_integer_iff (x : K) : x ∈ (valuation A K).integer ↔ ∃ a : A, algebraMap A K a = x :=
  by
  constructor
  · rintro ⟨c, rfl⟩
    use c
    rw [Algebra.smul_def, mul_one]
  · rintro ⟨c, rfl⟩
    use c
    rw [Algebra.smul_def, mul_one]

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