Commit 2023-12-11 09:59 7be3f993

feat(MonoidAlgebra): add AddMonoidAlgebra.lift_of' (#8938) Add AddMonoidAlgebra.lift_of'. simp can prove it but it's useful for rewriting right to left. Other changes:

• Move MonoidAlgebra.lift_of and prove it by simp to make it clear that simp can prove it.
• Stop abusing Multiplicative G = G in the statement of AddMonoidAlgebra.of'_eq_of.
• Reuse lemmas about MonoidAlgebra in some proofs about AddMonoidAlgebra.