card_inter_smul

Mathlib.Combinatorics.Additive.Convolution

URI: https://scilib.ai/kg/mathlib#Finset.card_inter_smul

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru