Theorem Cubic.card_roots_le

Modification history

2026-10-11 17:26
Mathlib/Algebra/CubicDiscriminant.lean
chore: use the `Finset.card` notation more widely (#44638) …
Modified Cubic.card_roots_leView on Github →
2023-03-28 10:43
Mathlib/Algebra/CubicDiscriminant.lean
feat: port Algebra.CubicDiscriminant (#3142)
Added Cubic.card_roots_leView on Github →