disc — Mathlib

English

The discriminant of a cubic with coefficients a,b,c,d is given by a^2 b^2 − 4 a c^3 − 4 b^3 d − 27 a^2 d^2 + 18 a b c d.

Русский

Дискриминант кубического полинома с коэффициентами a,b,c,d равен a^2 b^2 − 4 a c^3 − 4 b^3 d − 27 a^2 d^2 + 18 a b c d.

LaTeX

$$$$\\operatorname{disc}(P) = P.b^2 P.c^2 - 4 P.a P.c^3 - 4 P.b^3 P.d - 27 P.a^2 P.d^2 + 18 P.a P.b P.c P.d.$$$$

Lean4

/-- The discriminant of a cubic polynomial. -/
def disc {R : Type*} [Ring R] (P : Cubic R) : R :=
  P.b ^ 2 * P.c ^ 2 - 4 * P.a * P.c ^ 3 - 4 * P.b ^ 3 * P.d - 27 * P.a ^ 2 * P.d ^ 2 + 18 * P.a * P.b * P.c * P.d

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