weightedSumSquares — Mathlib

English

Discriminant under composition with a linear map f scales by det(f)^2.

Русский

Дискриминант при композиции с линейным отображением f масштабируется на det(f)^2.

LaTeX

$$discr_comp (f) : (Q.comp f).discr = det(f.toMatrix')^2 · Q.discr$$

Lean4

/-- 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. -/
def weightedSumSquares [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) : QuadraticMap R (ι → R) R :=
  ∑ i : ι, w i • (proj (R := R) (n := ι) i i)

Похожие утверждения