Theorems · Definition · number theory

QuadraticForm.weightedSumSquaresCongr

{ι : Type u_10} →
  {S : Type u_11} →
    {R : Type u_12} →
      [inst : Fintype ι] →
        [inst_1 : CommSemiring R] →
          [inst_2 : Monoid S] →
            [inst_3 : DistribMulAction S R] →
              [inst_4 : SMulCommClass S R R] →
                {w w' : ι → S} →
                  w = w' → (QuadraticMap.weightedSumSquares R w).IsometryEquiv (QuadraticMap.weightedSumSquares R w')

The isometry between two weighted sum of squares of equal weights.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeCommSemiringMonoidDistribMulActionSMulCommClass