den_mem — Mathlib

English

The relationship between denominator, valuation, and the algebra map expresses a standard fraction equality: f.den • f.val = algebraMap_A_to_Localization(f.num).

Русский

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

LaTeX

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

Lean4

theorem den_mem (f : HomogeneousLocalization 𝒜 x) : f.den ∈ x :=
  (Quotient.out f).den_mem

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