English
If the right cosets of s by elements of t are pairwise disjoint, then s.card divides (s * t).card.
Русский
Если правые косеты s по элементам t попарно непересекаются, то |s| делит |s·t|.
LaTeX
$$$((\\cdot \\; t)'' (s : Set \\alpha)).PairwiseDisjoint id \\rightarrow |s| \\mid |s \\cdot 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_mul_right {s t : Finset α} :
((· • t) '' (s : Set α)).PairwiseDisjoint id → t.card ∣ (s * t).card :=
card_dvd_card_image₂_right fun _ _ => mul_right_injective _
