Commit 2026-10-02 06:50 8e30cac8

View on Github →

chore(Algebra/QuadraticAlgebra): define all the casts through C (#43583) The casts into QuadraticAlgebra R a b were defined in two different ways, some through C and some through the anonymous constructor, which made the Algebra ℤ instances non-defeq at instance transparency. Using C everywhere fixes it, and an example records the defeq. Prepared with Claude Code 🤖

Estimated changes