Commit 2025-11-22 13:18 fe8d3134
View on Github →chore(Algebra): change two statements in CubicDiscriminant (#31912) The conclusions of the two lemmas do not mention x,y,z, and we make the assumption not mention x,y,z in this PR. The new and old assumptions are equivalent by Cubic.splits_iff_roots_eq_three earlier in the file. This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.