mem_support_iff — Mathlib

English

For f ∈ SkewMonoidAlgebra k G and a ∈ G, a is in f.support iff f.coeff(a) ≠ 0.

Русский

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

LaTeX

$$$ a \in f.\mathrm{support} \iff f.\mathrm{coeff}(a) \neq 0 $$$

Lean4

@[simp]
theorem mem_support_iff {f : SkewMonoidAlgebra k G} {a : G} : a ∈ f.support ↔ f.coeff a ≠ 0 :=
  by
  rcases f with ⟨⟩
  simp only [coeff, support_ofFinsupp, Finsupp.mem_support_iff, ne_eq]

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