support — Mathlib

English

For f ∈ SkewMonoidAlgebra k G with representation ⟨p⟩, the support of f is the support of p as a finsupp.

Русский

Для f ∈ SkewMonoidAlgebra k G с представлением f = ⟨p⟩ поддержка f равна поддержке p в Finsupp.

LaTeX

$$$ \mathrm{support}(f) = p.\mathrm{support} \quad \text{when } f = \langle p \rangle $$$

Lean4

/-- For `f : SkewMonoidAlgebra k G`, `f.support` is the set of all `a ∈ G` such that
`f.coeff a ≠ 0`. -/
def support : SkewMonoidAlgebra k G → Finset G
  | ⟨p⟩ => p.support

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