coe_to_intFractPair — Mathlib

English

Coercion respects the IntFractPair constructor across base rings: the coe of IntFractPair.mk b fr equals IntFractPair.mk b (↑fr).

Русский

Коэрцирование сохраняет конструктор IntFractPair: \nкоэрциa IntFractPair.mk b fr = IntFractPair.mk b (↑fr).

LaTeX

$$$\\\\forall {K} {\\\\beta} [\\\\oover K] [\\\\oover β] [Coe K β], \\\\forall {b : ℤ} {fr : K},\n (↑(IntFractPair.mk b fr) : IntFractPair β) = IntFractPair.mk b (↑fr : β)$$$

Lean4

@[simp, norm_cast]
theorem coe_to_intFractPair {b : ℤ} {fr : K} :
    (↑(IntFractPair.mk b fr) : IntFractPair β) = IntFractPair.mk b (↑fr : β) :=
  rfl

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