convolution_ne_zero

Mathlib.Combinatorics.Additive.Convolution

URI: https://scilib.ai/kg/mathlib#Finset.convolution_ne_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) \neq 0 \iff x \in A B $$$

Lean4

@[to_additive addConvolution_ne_zero]
theorem convolution_ne_zero : A.convolution B x ≠ 0 ↔ x ∈ A * B :=
  by
  suffices A.convolution B x ≠ 0 ↔ 0 < A.convolution B x by simp [this]
  cutsat

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

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

Разделы

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

Аффилиация

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