isSymm_iff

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

Symmetry of a bilinear form is equivalent to symmetry as a linear map.

Русский

Симметричность билинейной формы эквивалентна симметричности как линейного отображения.

LaTeX

$$IsSymm B \iff LinearMap.IsSymm B$$

Lean4

theorem isSymm_iff : IsSymm B ↔ LinearMap.IsSymm B := by simp [isSymm_def, LinearMap.isSymm_def]

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

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

Разделы

Аффилиация

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