coe_toPair

Mathlib.Algebra.ContinuedFractions.Basic

URI: https://scilib.ai/kg/mathlib#GenContFract.Pair.coe_toPair

Lean4

@[simp, norm_cast]
theorem coe_toPair {a b : α} : (↑(Pair.mk a b) : Pair β) = Pair.mk (a : β) (b : β) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru