English
In a finite index family, smul distributes across the piFinset of Finsets.
Русский
Для конечного индекса Smul распределяется через piFinset из Finset.
LaTeX
$$$\\pi\\mathrm{Finset} (i \\mapsto s_i \\;\\text{smul} \\; t_i) = (\\pi\\mathrm{Finset} s) \\;\\text{smul} \\; (\\pi\\mathrm{Finset} t)$$$
Lean4
/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
the size of `t` divides the size of `s • t`. -/
@[to_additive /-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily
distinct!), then the size of `t` divides the size of `s +ᵥ t`. -/
]
theorem card_dvd_card_smul_right {s : Finset α} :
((· • t) '' (s : Set α)).PairwiseDisjoint id → t.card ∣ (s • t).card :=
card_dvd_card_image₂_right fun _ _ => MulAction.injective _
