traceForm_isSymm

Mathlib.RingTheory.Trace.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.traceForm_isSymm

English

The trace form B(x,y) = Tr_{S/R}(xy) is symmetric: B(x,y) = B(y,x).

Русский

Следовая форма симметрична: B(x,y) = B(y,x).

LaTeX

$$$B(x,y) = B(y,x) \\quad \\text{where } B(x,y) = \\operatorname{trace}_{S/R}(xy)$$$

Lean4

theorem traceForm_isSymm : (traceForm R S).IsSymm :=
  ⟨fun _ _ => congr_arg (trace R S) (mul_comm _ _)⟩

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

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

Разделы

Аффилиация

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