Commit 2022-07-18 17:22 582e6672

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.