Mathlib Map

Theorems · Definition · field theory

Cubic.a

{R : Type u_1} → Cubic R → R

The degree-3 coefficient

Defined in
Mathlib.Algebra.CubicDiscriminant
Cited by
46 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Cubic.toPoly · cited by 88Cubic.toPolyCubic.map · cited by 13Cubic.mapCubic.discr · cited by 10Cubic.discrCubic.of_a_eq_zero · cited by 7Cubic.of_a_eq_zeroCubic.of_b_eq_zero · cited by 7Cubic.of_b_eq_zeroCubic.of_c_eq_zero · cited by 6Cubic.of_c_eq_zeroCubic.ext · cited by 5Cubic.extWeierstrassCurve.Affine.addPolynomial_slope · cited by 3Affine.addPolynomial_slopeCubic.eq_sum_three_roots · cited by 3Cubic.eq_sum_three_rootsCubic.leadingCoeff_of_a_ne_zero · cited by 3Cubic.leadingCoeff_of_a_n…Cubic.map_toPoly · cited by 3Cubic.map_toPolyCubic.degree_of_a_ne_zero · cited by 2Cubic.degree_of_a_ne_zeroCubic.leadingCoeff_of_b_ne_zero · cited by 2Cubic.leadingCoeff_of_b_n…Cubic.leadingCoeff_of_c_eq_zero · cited by 2Cubic.leadingCoeff_of_c_e…Cubic.leadingCoeff_of_c_ne_zero · cited by 2Cubic.leadingCoeff_of_c_n…Cubic · cited by 71CubicCubic.aCITED BYCITES

Cites1

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

  • Cubicstatement and proof · cited by 71

Cited by49

Results whose statement or proof uses this declaration.