mathlib

582e6672 - feat(algebraic_geometry/EllipticCurve): simplify definition of discriminant (#15365)

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](https://www.lmfdb.org/knowledge/show/ec.discriminant), and proves the equivalence to the (slightly reformatted) explicit polynomial in terms of the $a_i$'s.