support_one

Mathlib.Algebra.SkewMonoidAlgebra.Support

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.support_one

English

When 1 is nondegenerate (NeZero), the unit’s support is exactly {1}.

Русский

При условии, что 1 ненулевой, опора единицы равна {1}.

LaTeX

$$[NeZero (1) ] ⇒ (1 : SkewMonoidAlgebra k G).\\operatorname{support} = 1$$

Lean4

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

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

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

Разделы

Аффилиация

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