Commit 2026-07-23 16:42 aa96a837

feat(RingTheory/MonoidAlgebra): toAdditive as a BialgEquiv (#41413) Also add a few missing lemmas about the less bundled versions, make variable names follow the local file convention and explicit a missing argument. Also unprotected toMultiplicative and toAdditive because I do not see any reason why these should have been protected in the first place. From Toric