ofBaseChangeAux_ι — Mathlib

English

Under base change, the basic embedding ι_Q of the vector space V into CliffordAlgebra Q corresponds to embedding into the base-changed Clifford algebra via 1 ⊗ v, i.e., ι_Q(v) maps to ι_{Q.baseChange A}(1 ⊗ v).

Русский

При базовом изменении базисная вложенность ι_Q элемента v в CliffordAlgebra Q соответствует вложению в CliffordAlgebra(Q.baseChange A) через 1 ⊗ v: ι_Q(v) идёт в ι_{Q.baseChange A}(1 ⊗ v).

LaTeX

$$$\iota_Q(v) \mapsto \iota_{Q.baseChange A}(1 \otimes v)$$$

Lean4

@[simp]
theorem ofBaseChangeAux_ι (Q : QuadraticForm R V) (v : V) : ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (1 ⊗ₜ v) :=
  CliffordAlgebra.lift_ι_apply _ _ v

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