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)