Commit 2026-04-08 11:51 474ff4c9
View on Github →chore(Mathlib/Algebra/MonoidAlgebra/Basic.lean): automated extraction (#37797) This PR was automatically created from PR #28013 by @astrainfinita via a review comment by @jcommelin.
chore(Mathlib/Algebra/MonoidAlgebra/Basic.lean): automated extraction (#37797) This PR was automatically created from PR #28013 by @astrainfinita via a review comment by @jcommelin.