Mathlib Map

Theorems · Definition · field theory

Cubic.discr

{R : Type u_5} → [Ring R] → Cubic R → R

The discriminant of a cubic polynomial.

Defined in
Mathlib.Algebra.CubicDiscriminant
Cited by
10 results in Mathlib
Foundations
Depth 19 from the axioms · uses propext
Assumes
Ring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

WeierstrassCurve.twoTorsionPolynomial_discr · cited by 3WeierstrassCurve.twoTorsi…WeierstrassCurve.twoTorsionPolynomial_discr_isUnit · cited by 1WeierstrassCurve.twoTorsi…WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero · cited by 1WeierstrassCurve.twoTorsi…Cubic.discr_eq_prod_three_roots · cited by 1Cubic.discr_eq_prod_three…Cubic.discr_ne_zero_iff_roots_ne · cited by 1Cubic.discr_ne_zero_iff_r…Cubic.discr_ne_zero_iff_roots_nodup · cited by 1Cubic.discr_ne_zero_iff_r…WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero_of_isElliptic · cited by 0WeierstrassCurve.twoTorsi…WeierstrassCurve.twoTorsionPolynomial_discr_of_char_three · cited by 0WeierstrassCurve.twoTorsi…WeierstrassCurve.twoTorsionPolynomial_discr_of_char_two · cited by 0WeierstrassCurve.twoTorsi…Cubic.card_roots_of_discr_ne_zero · cited by 0Cubic.card_roots_of_discr…Ring · cited by 7463RingCubic · cited by 71CubicCubic.a · cited by 46Cubic.aCubic.b · cited by 32Cubic.bCubic.c · cited by 26Cubic.cCubic.d · cited by 21Cubic.dCubic.discrCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Ringstatement and proof · cited by 7,463
  • Cubicstatement and proof · cited by 71
  • Cubic.aproof · cited by 46
  • Cubic.bproof · cited by 32
  • Cubic.cproof · cited by 26
  • Cubic.dproof · cited by 21

Cited by10

Results whose statement or proof uses this declaration.