eq_num_div_den — Mathlib

English

Equality expressing the fundamental representation of an element by its numerator and denominator in the localization.

Русский

Эквивалентность, выражающая базовое представление элемента через его числитель и знаменатель в локализации.

LaTeX

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

Lean4

theorem eq_num_div_den (f : HomogeneousLocalization 𝒜 x) : f.val = Localization.mk f.num ⟨f.den, f.den_mem⟩ :=
  congr_arg HomogeneousLocalization.val (Quotient.out_eq' f).symm

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