Commit 2026-07-28 19:54 0ce898f5
View on Github →feat(RingTheory): bialgebra homs R[G] → R[H] are in bijection with group homs G → H (#41995)
... for abelian groups G and H. Furthermore, the convolution product on bialgebra homs corresponds to pointwise addition on group homs.
Also generate more lemmas through to_additive, remove some unused set_options and relocate MonoidAlgebra.toAdditive/AddMonoidAlgebra.toMultiplicative to existing sections.
From Toric