coe_of_rat_eq — Mathlib

English

If v equals ↑q, then the GenContFract representation of v equals that of q under the appropriate map.

Русский

Если v = ↑q, то представление GenContFract v совпадает с представлением q под соответствующим отображением.

LaTeX

$$$(v = (q : K)) \\rightarrow \\mathrm{GenContFract} (v) = \\mathrm{GenContFract} (q)$$$

Lean4

/-- Given `(v : K), (q : ℚ), and v = q`, we have that `of q = of v` -/
theorem coe_of_rat_eq (v_eq_q : v = (↑q : K)) : (⟨(of q).h, (of q).s.map (Pair.map (↑))⟩ : GenContFract K) = of v :=
  by
  rcases gcf_v_eq : of v with ⟨h, s⟩; subst v
  obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq
  simp [coe_of_s_rat_eq rfl, gcf_v_eq]

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