deg — Mathlib

English

Equality expressing that the value equals the canonical numerator-denominator construction: val(f) = Localization.mk f.num ⟨f.den, f.den_mem⟩.

Русский

Равенство, выражающее, что значение равно канонической константе числителя и знаменателя: val(f) = Localization.mk f.num ⟨f.den, f.den_mem⟩.

LaTeX

$$$\\mathrm{val}(f) = \\mathrm{Localization.mk}(f.\\mathrm{num}, \\langle f.\\mathrm{den}, f.\\mathrm{den\_mem} \\rangle)$$$

Lean4

/-- For an element in `HomogeneousLocalization x`, degree is the natural number `i` such that
  `𝒜 i` contains both numerator and denominator. -/
def deg (f : HomogeneousLocalization 𝒜 x) : ι :=
  (Quotient.out f).deg

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