Commit 2026-07-07 03:37 f4e566ca

feat(Algebra/MonoidAlgebra): more general algHom_ext (#41412) Generalise algHom_ext and algHom_ext from R[M] →ₐ[R] A to A[M] →ₐ[R] B by adding a second hypothesis that is automatically satisfied for R[M] →ₐ[R] A (see AlgHom.ext_id). Since the new extensionality lemma is more general, it applies in a bunch more places. Unfortunately, if it is stated using MonoidAlgebra.of then it isn't additivisable, meaning that a lot of previously additivised lemmas must now be written by hand. I therefore decided to drop the of spelling by unbundling the first hypothesis. This is justified by the fact that the users of the more bundled ext lemma are for M := Nat, Int or Free(Abelian)Group, none of which can be additivised. algHom_ext is now the partially bundled version, tagged with ext, and algHom_ext' the fully bundled version. From Toric