Commit 2025-12-16 09:36 915cd38e

View on Github →

chore: remove QuadraticAlgebra.coe (#32797) In the case R is ℤ or ℚ (that is very common in number theory) one now has two coercions R → QuadraticAlgebra R a b, and this is in practice very annoying. We also add a warning about a diamond for Algebra ℚ (QuadraticAlgebra a b). Discovered at ItaLean2025.

Estimated changes

deleted theorem QuadraticAlgebra.norm_coe
added theorem QuadraticAlgebra.C_add
added theorem QuadraticAlgebra.C_inj
added theorem QuadraticAlgebra.C_mul
added theorem QuadraticAlgebra.C_neg
added theorem QuadraticAlgebra.C_one
added theorem QuadraticAlgebra.C_pow
added theorem QuadraticAlgebra.C_sub
deleted theorem QuadraticAlgebra.coe_add
deleted theorem QuadraticAlgebra.coe_inj
deleted theorem QuadraticAlgebra.coe_mul
deleted theorem QuadraticAlgebra.coe_neg
deleted theorem QuadraticAlgebra.coe_one
deleted theorem QuadraticAlgebra.coe_pow
deleted theorem QuadraticAlgebra.coe_smul
deleted theorem QuadraticAlgebra.coe_sub
deleted theorem QuadraticAlgebra.coe_zero
added theorem QuadraticAlgebra.im_C
deleted theorem QuadraticAlgebra.im_coe
added theorem QuadraticAlgebra.re_C
deleted theorem QuadraticAlgebra.re_coe
deleted theorem QuadraticAlgebra.smul_coe