eq_iff

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.IsRefl.eq_iff

English

Restriction of a reflexive form to a submodule preserves the reflexivity property.

Русский

Ограничение рефлексивной формы к подмодулю сохраняет свойство рефлексивности.

LaTeX

$$$\\text{If } B \\text{ is reflexive, then } (B\\!\\restriction_{p}) \\text{ is reflexive for any submodule } p.$$$

Lean4

theorem eq_iff {x y} : B x y = 0 ↔ B y x = 0 :=
  ⟨H x y, H y x⟩

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

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

Разделы

Аффилиация

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