val — Mathlib

English

The valuation of a canonical representative mk i equals Localization.mk(i.num, i.den_mem).

Русский

Оценка mk i равна Localization.mk (i.num) (i.den_mem).

LaTeX

$$$\\mathrm{val}(\\mathrm{mk}(i)) = \\mathrm{Localization.mk}(i.\\mathrm{num}) \\,⟨i.\\mathrm{den}, i.\\mathrm{den\\,mem}\\rangle$$$

Lean4

/-- View an element of `HomogeneousLocalization 𝒜 x` as an element of `Aₓ` by forgetting that the
numerator and denominator are of the same grading.
-/
def val (y : HomogeneousLocalization 𝒜 x) : at x :=
  Quotient.liftOn' y (NumDenSameDeg.embedding 𝒜 x) fun _ _ => id

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