symm_apply_apply

Mathlib.Algebra.Module.Equiv.Defs

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

English

The AddEquiv corresponding to e symm equals the symm of the AddEquiv corresponding to e.

Русский

AddEquiv, соответствующий e.symm, равен симм AddEquiv, соответствующему e.

LaTeX

$$$\\mathrm{coe\\_toAddEquiv\\_symm}: (e_{12}.symm) = (e_{12})^{\\mathrm{symm}}$$$

Lean4

@[simp]
theorem symm_apply_apply (b : M) : e.symm (e b) = b :=
  e.left_inv b

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

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

Разделы

Аффилиация

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