coe_of_rat_eq — Mathlib

English

If v = ↑q for some rational q, then mapping of IntFractPair.of q through the canonical map equals IntFractPair.of v.

Русский

Если v = ↑q для некоторого рационального q, то отображение IntFractPair.of q через каноническую карту совпадает с IntFractPair.of v.

LaTeX

$$$(v = (q : K)) \\rightarrow ((IntFractPair.of q).map Fr (↑) : IntFractPair K) = IntFractPair.of v$$$

Lean4

theorem coe_of_rat_eq (v_eq_q : v = (↑q : K)) : ((IntFractPair.of q).mapFr (↑) : IntFractPair K) = IntFractPair.of v :=
  by simp [IntFractPair.of, v_eq_q]

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