Theorems · Inductive type · field theory
Cubic
Type u_1 → Type u_1
The structure representing a cubic polynomial.
- Defined in
- Mathlib.Algebra.CubicDiscriminant
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by87
Results whose statement or proof uses this declaration.
- Cubic.toPolystatement and proof · cited by 88
- Cubic.astatement and proof · cited by 46
- Cubic.bstatement and proof · cited by 32
- Cubic.cstatement and proof · cited by 26
- Cubic.dstatement and proof · cited by 21
- Cubic.rootsstatement and proof · cited by 14
- Cubic.mapstatement and proof · cited by 13
- Cubic.discrstatement and proof · cited by 10
- WeierstrassCurve.twoTorsionPolynomialstatement · cited by 9
- Cubic.of_a_eq_zerostatement and proof · cited by 7
- Cubic.of_b_eq_zerostatement and proof · cited by 7
- Cubic.of_c_eq_zerostatement and proof · cited by 6