Theorem Finset.card_smul_finset₀

Modification history

2026-10-11 17:26
Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean
chore: use the `Finset.card` notation more widely (#44638) …
Modified Finset.card_smul_finset₀View on Github →
2026-04-20 10:00
Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean
feat(Algebra/GroupWithZero/Action/Pointwise/Finset): add ₀ variants (#38103) …
Added Finset.card_smul_finset₀View on Github →