ofBaseChange_tmul_ι — Mathlib

English

The composite of the ι-embedding with base change behaves compatibly: the base-changed embedding of z maps to z ⊗ ι_Q v in the target CliffordAlgebra.

Русский

Сведение вложения ι после изменения базы совместимо: отображение z ⊗ ι_Q v соответствует базово-измененному вложению.

LaTeX

$$$\;toBaseChange A Q (z \otimes_{} ι_Q(v)) = ι(Q.baseChange A)(z \otimes v)$$$

Lean4

@[simp]
theorem ofBaseChange_tmul_ι (Q : QuadraticForm R V) (z : A) (v : V) :
    ofBaseChange A Q (z ⊗ₜ ι Q v) = ι (Q.baseChange A) (z ⊗ₜ v) :=
  by
  change algebraMap _ _ z * ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)
  rw [ofBaseChangeAux_ι, ← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

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