symm

Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

URI: https://scilib.ai/kg/mathlib#QuadraticMap.Equivalent.symm

English

The reflexive equivalence between a quadratic map and itself holds, i.e., Q.Equivalent Q.

Русский

Рефлексивная эквивалентность квадратичной карты самой себе выполняется: Q.Equivalent Q.

LaTeX

$$$\mathrm{refl}(Q) : Q.Equivalent Q$$$

Lean4

@[symm]
theorem symm (h : Q₁.Equivalent Q₂) : Q₂.Equivalent Q₁ :=
  h.elim fun f => ⟨f.symm⟩

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

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

Разделы

Аффилиация

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