Commit 2025-10-20 10:08 147c92b3

View on Github →

chore: change disc to discr to denote the discriminant (#30709) See Zulip

Estimated changes

Modified Mathlib/Algebra/CubicDiscriminant.lean

deleted theorem Cubic.card_roots_of_disc_ne_zero

added theorem Cubic.card_roots_of_discr_ne_zero

deleted def Cubic.disc

deleted theorem Cubic.disc_eq_prod_three_roots

deleted theorem Cubic.disc_ne_zero_iff_roots_ne

deleted theorem Cubic.disc_ne_zero_iff_roots_nodup

added def Cubic.discr

added theorem Cubic.discr_eq_prod_three_roots

added theorem Cubic.discr_ne_zero_iff_roots_ne

added theorem Cubic.discr_ne_zero_iff_roots_nodup

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

deleted theorem WeierstrassCurve.twoTorsionPolynomial_disc

deleted theorem WeierstrassCurve.twoTorsionPolynomial_disc_isUnit

deleted theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero

deleted theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero_of_isElliptic

deleted theorem WeierstrassCurve.twoTorsionPolynomial_disc_of_char_three

deleted theorem WeierstrassCurve.twoTorsionPolynomial_disc_of_char_two

added theorem WeierstrassCurve.twoTorsionPolynomial_discr

added theorem WeierstrassCurve.twoTorsionPolynomial_discr_isUnit

added theorem WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero

added theorem WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero_of_isElliptic

added theorem WeierstrassCurve.twoTorsionPolynomial_discr_of_char_three

added theorem WeierstrassCurve.twoTorsionPolynomial_discr_of_char_two

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Disc.lean

deleted theorem Matrix.disc_fin_two

deleted theorem Matrix.disc_of_card_eq_two

added theorem Matrix.discr_fin_two

added theorem Matrix.discr_of_card_eq_two

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

modified def Matrix.IsElliptic

modified def Matrix.IsHyperbolic

modified def Matrix.IsParabolic

deleted theorem Matrix.disc_conj'

deleted theorem Matrix.disc_conj

added theorem Matrix.discr_conj'

added theorem Matrix.discr_conj

deleted theorem Matrix.sub_scalar_sq_eq_disc

added theorem Matrix.sub_scalar_sq_eq_discr

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

deleted theorem Polynomial.disc_C

deleted theorem Polynomial.disc_of_degree_eq_one

deleted theorem Polynomial.disc_of_degree_eq_three

deleted theorem Polynomial.disc_of_degree_eq_two

added theorem Polynomial.discr_C

added theorem Polynomial.discr_of_degree_eq_one

added theorem Polynomial.discr_of_degree_eq_three

added theorem Polynomial.discr_of_degree_eq_two

Modified Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean