flip_flip

Mathlib.LinearAlgebra.BilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.flip_flip

English

The flip operation is an involution: flipHom.trans flipHom = LinearEquiv.refl R (BilinForm R M).

Русский

Операция поворота является инволюцией: flipHom.trans flipHom = линейное отображение-тождество.

LaTeX

$$$$flipHom.\text{trans}(flipHom) = \text{LinearEquiv.refl } R (BilinForm R M)$$$$

Lean4

theorem flip_flip : flipHom.trans flipHom = LinearEquiv.refl R (BilinForm R M) :=
  by
  ext A
  simp

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

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

Разделы

Аффилиация

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