support_one — Mathlib

English

For a ring k and any G, the support of 1 in k[G] lies in {0}, that is, only the neutral element may appear with nonzero coefficient.

Русский

Для кольца k и любой группы/моноида G опора 1 в k[G] уделяет только нейтральному элементу.

LaTeX

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

Lean4

@[simp]
theorem support_one [Zero G] [NeZero (1 : k)] : (1 : k[G]).support = 0 :=
  Finsupp.support_single_ne_zero _ one_ne_zero

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