traceForm_apply

Mathlib.RingTheory.Trace.Defs

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

English

For a basis b of S over R, the matrix of traceForm with respect to b has entries (i,j) equal to Tr_{S/R}(b_i b_j).

Русский

Для базиса b над S/ R матрица traceForm имеет элементы a_{ij} = Tr_{S/R}(b_i b_j).

LaTeX

$$$\\mathrm{toMatrix}_{b}(\\mathrm{traceForm}_{R,S})_{ij} = \\operatorname{trace}_{R,S}(b_i b_j)$$$

Lean4

@[simp]
theorem traceForm_apply (x y : S) : traceForm R S x y = trace R S (x * y) :=
  rfl

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

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

Разделы

Аффилиация

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