Theorems · Definition · number theory

QuadraticForm.tensorComm

{R : Type uR} →
  {M₁ : Type uM₁} →
    {M₂ : Type uM₂} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                [inst_5 : Invertible 2] →
                  (Q₁ : QuadraticForm R M₁) →
                    (Q₂ : QuadraticForm R M₂) → QuadraticMap.IsometryEquiv (Q₁.tmul Q₂) (Q₂.tmul Q₁)

TensorProduct.comm preserves tensor products of quadratic forms.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModuleInvertible