English
If left cosets by elements of s are pairwise disjoint, then t.card divides (s • t).card.
Русский
Если левые косетки элементов s по t взаимно непересекаются, то |t| делит |s • t|.
LaTeX
$$$((\\cdot \\; smul\\; t)'' (s : Set \\alpha)).PairwiseDisjoint id \\rightarrow |t| \\mid |s \\cdot t|$$$
Lean4
/-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily distinct!), then
the size of `s` divides the size of `s * t`. -/
@[to_additive /-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily
distinct!), then the size of `s` divides the size of `s + t`. -/
]
theorem card_dvd_card_mul_left {s t : Finset α} :
((fun b => s.image fun a => a * b) '' (t : Set α)).PairwiseDisjoint id → s.card ∣ (s * t).card :=
card_dvd_card_image₂_left fun _ _ => mul_left_injective _
