flip_apply

Mathlib.LinearAlgebra.BilinearForm.Basic

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

English

For any A, x, y, flipHom A x y = A y x.

Русский

Для любой A, x, y: flipHom A x y = A y x.

LaTeX

$$$$flipHom A\, x\, y = A\, y\, x$$$$

Lean4

@[simp]
theorem flip_apply (A : BilinForm R M) (x y : M) : flipHom A x y = A y x :=
  rfl

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

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

Разделы

Аффилиация

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