Theorem Cubic.degree_of_c_ne_zero'

Modification history

2025-05-15 09:40

Mathlib/Algebra/CubicDiscriminant.lean

chore: remove `@[simp]` from lemmas that `simp [*]` can prove (#24926)

Modified Cubic.degree_of_c_ne_zero'View on Github →

2023-03-28 10:43

Mathlib/Algebra/CubicDiscriminant.lean

feat: port Algebra.CubicDiscriminant (#3142)

Added Cubic.degree_of_c_ne_zero'View on Github →