awayMapAux_mk — Mathlib

English

The range of awayMapAux is contained in the range of the valuation map.

Русский

Область значений awayMapAux вложена в область значений отображения val.

LaTeX

$$$$ \mathrm{range}(\text{awayMapAux}) \subseteq \mathrm{range}(\mathrm{val}). $$$$

Lean4

theorem awayMapAux_mk (n a i hi) :
    awayMapAux 𝒜 ⟨_, hx⟩ (mk ⟨n, a, ⟨f ^ i, hi⟩, ⟨i, rfl⟩⟩) =
      Localization.mk (a * g ^ i) ⟨x ^ i, (Submonoid.mem_powers_iff _ _).mpr ⟨i, rfl⟩⟩ :=
  by
  have :
    algebraMap A (Localization.Away x) f *
        (Localization.mk g ⟨f * g, (Submonoid.mem_powers_iff _ _).mpr ⟨1, by simp [hx]⟩⟩) =
      1 :=
    by
    rw [← Algebra.smul_def, Localization.smul_mk]
    exact Localization.mk_self ⟨f * g, _⟩
  simp [awayMapAux]
  rw [Localization.awayLift_mk (hv := this), ← Algebra.smul_def, Localization.mk_pow, Localization.smul_mk]
  subst hx
  rfl

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