Commit 2026-04-09 13:40 caf4ab9d
View on Github →chore(Mathlib/Data/Finsupp/Indicator.lean): automated extraction (#37811) This PR was automatically created from PR #28013 by @astrainfinita via a review comment by @jcommelin.
chore(Mathlib/Data/Finsupp/Indicator.lean): automated extraction (#37811) This PR was automatically created from PR #28013 by @astrainfinita via a review comment by @jcommelin.