weight_single_index

Mathlib.Data.Finsupp.Weight

URI: https://scilib.ai/kg/mathlib#Finsupp.weight_single_index

← MathLib Explorer

English

For any index s and weight c, weight w (Pi.single s c) equals c times w(s).

Русский

Для любого индекса s и веса c имеет место weight w (Pi.single s c) = c • w(s).

LaTeX

$$weight w (Finsupp.single s c) = c • w s$$

Lean4

theorem weight_single_index [DecidableEq σ] (s : σ) (c : M) (f : σ →₀ R) : weight (Pi.single s c) f = f s • c :=
  linearCombination_single_index σ M R c s f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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