valuation_eq_one_iff — Mathlib

English

The canonical map from a valuation subring to the ambient field is the identity on the underlying elements.

Русский

Каноническое отображение из оценочного подкольца в тело есть тождественное на базовых элементах.

LaTeX

$$$R.subtype =\mathrm{incl}$ on $R$$$

Lean4

theorem valuation_eq_one_iff (a : A) : IsUnit a ↔ A.valuation a = 1 :=
  ⟨fun h => A.valuation_unit h.unit, fun h =>
    by
    have ha : (a : K) ≠ 0 := by
      intro c
      rw [c, A.valuation.map_zero] at h
      exact zero_ne_one h
    have ha' : (a : K)⁻¹ ∈ A := by rw [← valuation_le_one_iff, map_inv₀, h, inv_one]
    apply isUnit_of_mul_eq_one a ⟨a⁻¹, ha'⟩; ext; simp [field]⟩

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