toEquiv_trans

Mathlib.Algebra.AddConstMap.Equiv

URI: https://scilib.ai/kg/mathlib#AddConstEquiv.toEquiv_trans

English

The toEquiv map preserves composition: (e1.trans e2).toEquiv = e1.toEquiv.trans e2.toEquiv.

Русский

Отображение toEquiv сохраняет композицию: (e1.trans e2).toEquiv = e1.toEquiv.trans e2.toEquiv.

LaTeX

$$$ (e_1.trans e_2).toEquiv = e_1.toEquiv.trans e_2.toEquiv $$$

Lean4

@[simp]
theorem toEquiv_trans (e₁ : G ≃+c[a, b] H) (e₂ : H ≃+c[b, c] K) : (e₁.trans e₂).toEquiv = e₁.toEquiv.trans e₂.toEquiv :=
  rfl

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

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

Разделы

Аффилиация

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