discr — Mathlib

English

Scaling a quadratic map by a scalar a scales its discriminant by a^{card n}.

Русский

Масштабирование квадратичной карты на скаляр a масштабирует её дискриминант на a^{card n}.

LaTeX

$$discr(a • Q) = a^{|n|} · discr(Q)$$

Lean4

/-- The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial. -/
def discr (Q : QuadraticMap R (n → R) R) : R :=
  Q.toMatrix'.det

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