support_one_subset — Mathlib

English

The support of the unit element 1 in k[G] is contained in the singleton {0}, i.e., it only has a nonzero coefficient at the identity of G when G is additive.

Русский

Опора элемента единицы 1 в k[G] содержится в множества {0}, то есть единственный ненулевой коэффициент расположен в нейтральном элементе G.

LaTeX

$$$\\operatorname{supp}(1) \\subseteq \\{0\\}$$$

Lean4

theorem support_one_subset [Zero G] : (1 : k[G]).support ⊆ 0 :=
  Finsupp.support_single_subset

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