Commit 2026-05-12 10:45 53f8a93a
View on Github →chore(Mathlib/Algebra/MonoidAlgebra/MapDomain.lean): automated extraction (#39237) This PR was automatically created from PR #28013 by @astrainfinita via a review comment by @jcommelin.
chore(Mathlib/Algebra/MonoidAlgebra/MapDomain.lean): automated extraction (#39237) This PR was automatically created from PR #28013 by @astrainfinita via a review comment by @jcommelin.