flip_isRefl_iff

Mathlib.LinearAlgebra.SesquilinearForm.Basic

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

English

The flip form is reflexive if and only if the original form is reflexive.

Русский

Переставленная форма является рефлексивной тогда и только тогда, когда исходная форма рефлексивна.

LaTeX

$$$(B.flip).IsRefl \\iff B.IsRefl$$$

Lean4

@[simp]
theorem flip_isRefl_iff : B.flip.IsRefl ↔ B.IsRefl :=
  ⟨fun h x y H ↦ h y x ((B.flip_apply _ _).trans H), fun h x y ↦ h y x⟩

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

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

Разделы

Аффилиация

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