coe_toEquiv_trans

Mathlib.RingTheory.Bialgebra.Equiv

URI: https://scilib.ai/kg/mathlib#BialgEquiv.coe_toEquiv_trans

English

Equality of Equiv from trans equals the trans of Equivs (redundant statement for consistency).

Русский

Равенство эквив из транспозитной композиции равно транспозитной композиции эквив(повтор).

LaTeX

$$$\\text{trans\_toEquiv} = \\text{toEquiv\_trans}$$$

Lean4

@[simp]
theorem coe_toEquiv_trans : (e₁₂ : A ≃ B).trans e₂₃ = (e₁₂.trans e₂₃ : A ≃ C) :=
  rfl

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

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

Разделы

Аффилиация

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