Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-18 17:22 582e6672

View on Github →

feat(algebraic_geometry/EllipticCurve): simplify definition of discriminant (#15365) This replaces the definition with a nested let definition more similar to the definition on the LMFDB page on discriminants, and proves the equivalence to the (slightly reformatted) explicit polynomial in terms of the $a_i$'s.

Estimated changes