Commit 2026-10-21 19:58 5f7b4198

View on Github →

feat(Algebra/QuadraticAlgebra): classify quadratic algebras over ℚ (#42393) Every QuadraticAlgebra ℚ a b with nonzero discriminant is isomorphic to a standard form QuadraticAlgebra ℚ d 0 for a squarefree integer d, and this d is a complete invariant. Thus quadratic algebras over ℚ are classified by squarefree integers.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/QuadraticAlgebra/Rat.lean

added theorem QuadraticAlgebra.Rat.exists_squarefree_algEquiv

added theorem QuadraticAlgebra.Rat.nonempty_algEquiv_iff

Modified Mathlib/Algebra/Squarefree/Basic.lean

added theorem IsSquare.of_mul_right

Created Mathlib/Data/Rat/Squarefree.lean

added theorem Rat.sq_mul_squarefree_unique

Modified Mathlib/RingTheory/Int/Basic.lean

added theorem Int.eq_of_squarefree_of_isSquare_mul

Modified Mathlib/RingTheory/Localization/NumDen.lean

added theorem IsFractionRing.exists_sq_mul_squarefree