card_smul_inter — Mathlib

English

For A,B ⊆ G finite and x ∈ G, the cardinality of (x • A) ∩ B equals A * B⁻¹ evaluated at x⁻¹.

Русский

Для конечных A,B ⊆ G и x ∈ G кардинальность (x • A) ∩ B равна (A * B⁻¹)(x⁻¹).

LaTeX

$$$ |(x \cdot A) \cap B| = (A * B^{-1})(x^{-1}) $$$

Lean4

@[to_additive]
theorem card_smul_inter (A B : Finset G) (x : G) : #((x • A) ∩ B) = A.convolution B⁻¹ x⁻¹ := by
  simpa using card_smul_inter_smul _ _ x 1

Похожие утверждения