Theorems · Definition · number theory

QuadraticMap.weightedSumSquares

{S : Type u_1} →
  (R : Type u_3) →
    [inst : CommSemiring R] →
      {ι : Type u_8} →
        [Fintype ι] →
          [inst_2 : Monoid S] →
            [inst_3 : DistribMulAction S R] → [SMulCommClass S R R] → (ι → S) → QuadraticMap R (ι → R) R

The weighted sum of squares with respect to some weight as a quadratic form. The weights are applied using •; typically this definition is used either with S = R or [Algebra S R], although this is stated more generally.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

18 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringFintypeMonoidDistribMulActionSMulCommClass