support_ofFinsupp

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

For p ∈ Finsupp G k, the support of ⟨p⟩ equals p.support.

Русский

Для p ∈ Finsupp G k, поддержка ⟨p⟩ равна p.support.

LaTeX

$$$ \mathrm{support}(\langle p \rangle) = p.\mathrm{support} $$$

Lean4

@[simp]
theorem support_ofFinsupp (p) : support (⟨p⟩ : SkewMonoidAlgebra k G) = p.support := by rw [support]

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

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

Разделы

Аффилиация

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