ofBaseChange_toBaseChange — Mathlib

English

The composition of the base-change morphism with itself yields the identity on the tensor product representation, reflecting the bidirectional compatibility of changing bases in Clifford algebras.

Русский

Сочетание базовых отображений при изменении баз даёт тождественность на тензорном произведении, демонстрируя двунаправленную совместимость изменения баз в Клиффордовых алгебрах.

LaTeX

$$$(toBaseChange A Q) \circ (toBaseChange A Q) = \mathrm{Id}$$$

Lean4

@[simp]
theorem ofBaseChange_toBaseChange (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
    ofBaseChange A Q (toBaseChange A Q x) = x :=
  AlgHom.congr_fun (ofBaseChange_comp_toBaseChange A Q :) x

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