convolution_eq_zero

Mathlib.Combinatorics.Additive.Convolution

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

← MathLib Explorer

English

For A,B ⊆ G finite and x ∈ G, A * B(x) = 0 iff x ∉ AB.

Русский

Для конечных A,B ⊆ G и x ∈ G, A * B(x) = 0 тогда и только тогда, когда x ∉ AB.

LaTeX

$$$ (A * B)(x) = 0 \iff x \notin AB $$$

Lean4

@[to_additive (attr := simp) addConvolution_eq_zero]
theorem convolution_eq_zero : A.convolution B x = 0 ↔ x ∉ A * B := by simp [← convolution_ne_zero]

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

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

Разделы

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

Аффилиация

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