mul_eq_comp

Mathlib.LinearAlgebra.RootSystem.Hom

URI: https://scilib.ai/kg/mathlib#RootPairing.Equiv.mul_eq_comp

English

For P, x, y, the product of two equivalences equals their composition.

Русский

Для эквивалентностей P, x, y произведение равно композиции.

LaTeX

$$$ x \\; * \\; y = x \\circ y $$$

Lean4

@[simp]
theorem mul_eq_comp {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) : x * y = Equiv.comp x y :=
  rfl

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

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

Разделы

Аффилиация

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