Theorems · Definition · number theory

QuadraticMap.Isometry.tmul

{R : Type uR} →
  {M₁ : Type uM₁} →
    {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 : AddCommGroup M₄] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module R M₄] →
                            [inst_9 : Invertible 2] →
                              {Q₁ : QuadraticForm R M₁} →
                                {Q₂ : QuadraticForm R M₂} →
                                  {Q₃ : QuadraticForm R M₃} →
                                    {Q₄ : QuadraticForm R M₄} → (Q₁ →qᵢ Q₂) → (Q₃ →qᵢ Q₄) → Q₁.tmul Q₃ →qᵢ Q₂.tmul Q₄

TensorProduct.map for QuadraticForm.Isometrys

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleModuleInvertible