eq_symm_comp

Mathlib.Algebra.Module.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#LinearEquiv.eq_symm_comp

English

There is a symmetric equality between the composition and the identity map.

Русский

Существуют симметричные равенства между композицией и тождественным отображением.

LaTeX

$$$e \\;\\text{trans} \\; e^{-1} = \\mathrm{id}$$$

Lean4

theorem eq_symm_comp {α : Type*} (f : α → M₁) (g : α → M₂) : f = e₁₂.symm ∘ g ↔ e₁₂ ∘ f = g :=
  e₁₂.toEquiv.eq_symm_comp f g

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

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

Разделы

Аффилиация

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