den_smul_val — Mathlib

English

Relation between denominator, val, and algebra map: f.den • f.val = algebraMap_A_to_Localization(f.num).

Русский

Соотношение между знаменателем, val и алгебраическим отображением: f.den • f.val = algebraMap_A_to_Localization(f.num).

LaTeX

$$$f.\\mathrm{den} \\; \\smul \\; f.\\mathrm{val} = \\mathrm{algebraMap}_{A \\to \\mathrm{Localization}(x)}(f.\\mathrm{num})$$$

Lean4

theorem den_smul_val (f : HomogeneousLocalization 𝒜 x) : f.den • f.val = algebraMap _ _ f.num :=
  by
  rw [eq_num_div_den, Localization.mk_eq_mk', IsLocalization.smul_mk']
  exact IsLocalization.mk'_mul_cancel_left _ ⟨_, _⟩

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