Commit 2026-04-20 10:00 730f55bd

View on Github →

feat(Algebra/GroupWithZero/Action/Pointwise/Finset): add ₀ variants (#38103) These lemmas all have Group versions, and so we add GroupWithZero variants.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean

added theorem Finset.card_dvd_card_smul_right₀

added theorem Finset.card_smul_finset₀

added theorem Finset.smul_finset_eq_univ₀