support_toFinsupp

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

For p ∈ SkewMonoidAlgebra k G, the toFinsupp image and the SkewMonoidAlgebra support agree: toFinsupp(p).support = p.support.

Русский

Для p ∈ SkewMonoidAlgebra k G, совпадают поддержки: toFinsupp(p).support = p.support.

LaTeX

$$$ p^{\mathrm{toFinsupp}}.\mathrm{support} = p.\mathrm{support} $$$

Lean4

theorem support_toFinsupp (p : SkewMonoidAlgebra k G) : p.toFinsupp.support = p.support := by rw [support]

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

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

Разделы

Аффилиация

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