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 🤖