Theorems · Definition · number theory

QuadraticForm.tensorAssoc

{R : Type uR} →
  {M₁ : Type uM₁} →
    {M₂ : Type uM₂} →
      {M₃ : Type uM₃} →
        [inst : CommRing R] →
          [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₃] →
                      [inst_7 : Invertible 2] →
                        (Q₁ : QuadraticForm R M₁) →
                          (Q₂ : QuadraticForm R M₂) →
                            (Q₃ : QuadraticForm R M₃) →
                              QuadraticMap.IsometryEquiv ((Q₁.tmul Q₂).tmul Q₃) (Q₁.tmul (Q₂.tmul Q₃))

TensorProduct.assoc preserves tensor products of quadratic forms.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleInvertible