isSymm_def

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.isSymm_def

English

IsSymm(B) is equivalent to the condition I(B(x,y)) = B(y,x) for all x,y.

Русский

IsSymm(B) эквивалентно условию I(B(x,y)) = B(y,x) для всех x,y.

LaTeX

$$$B.IsSymm \\iff \\forall x,y, I(B(x,y)) = B(y,x)$$$

Lean4

theorem isSymm_def {B : M →ₛₗ[I] M →ₗ[R] R} : B.IsSymm ↔ ∀ x y, I (B x y) = B y x :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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

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

Разделы

Аффилиация

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