Commit 2026-10-02 10:35 af914e73

chore(Algebra/QuadraticAlgebra): make C the simp normal form (#44417) Following #43583, add the simp lemma QuadraticAlgebra.mk_zero_eq_C : ⟨r, 0⟩ = C r, as suggested by @Vierkantor, and state algebraMap_eq with C. This PR also fixes a simp loop on the casts from ℚ≥0 and ℚ: simp was rewriting such a cast into C of the cast, and then back into the cast. For example, simp could not prove that the real part of a rational cast is that rational. Prepared with Claude Code 🤖