Def AddMonoidAlgebra.comapMulSemiringAction

Modification history

2026-10-20 15:24

Mathlib/Algebra/MonoidAlgebra/Basic.lean

chore(Algebra/MonoidAlgebra/Basic): automated extraction from #28013 (#45088) …

Added AddMonoidAlgebra.comapMulSemiringAction View on Github →