notMem_support_iff

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

For f ∈ SkewMonoidAlgebra k G and a ∈ G, a ∉ f.support iff f.coeff(a) = 0.

Русский

Для f ∈ SkewMonoidAlgebra k G и a ∈ G: a ∉ support(f) тогда и только тогда, когда f.coeff(a) = 0.

LaTeX

$$$ a \notin f.\mathrm{support} \iff f.\mathrm{coeff}(a) = 0 $$$

Lean4

theorem notMem_support_iff {f : SkewMonoidAlgebra k G} {a : G} : a ∉ f.support ↔ f.coeff a = 0 := by
  simp only [mem_support_iff, ne_eq, not_not]

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

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

Разделы

Аффилиация

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