degree_eq_weight_one

Mathlib.Data.Finsupp.Weight

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

← MathLib Explorer

English

The degree of f equals the weight of the constant-one function on σ: deg f = weight(1).

Русский

Степень f равна весу константной единицы на σ: deg f = weight(1).

LaTeX

$$$\deg f = \operatorname{weight}(\mathbf{1}_{\sigma})$$$

Lean4

theorem degree_eq_weight_one {R : Type*} [Semiring R] : degree (R := R) (σ := σ) = weight (fun _ ↦ 1) :=
  by
  ext d
  simp only [degree, weight_apply, smul_eq_mul, mul_one, Finsupp.sum]

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

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

Разделы

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

Аффилиация

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