Theorems · Theorem · ring theory

CliffordAlgebra.equivOfIsometry_trans

∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
  (e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂) (e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃),
  (CliffordAlgebra.equivOfIsometry e₁₂).trans (CliffordAlgebra.equivOfIsometry e₂₃) =
    CliffordAlgebra.equivOfIsometry (e₁₂.trans e₂₃)

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupAddCommGroupAddCommGroupModuleModuleModule