coe_of_h_rat_eq — Mathlib

English

If v = ↑q for rational q, then the h-component of the of q equals the h-component of of v after casting rationals.

Русский

Если v = ↑q для рационального q, то компонент h конвергента of q совпадает с компонентом h конвергента of v после приведения к рациональным числам.

LaTeX

$$$(v = (q : K)) \\rightarrow (\\uparrow ((of q).h : \\mathbb{Q})) = (of v).h$$$

Lean4

theorem coe_of_h_rat_eq (v_eq_q : v = (↑q : K)) : (↑((of q).h : ℚ) : K) = (of v).h := by simp_all

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