weightedTotalDegree_one — Mathlib

English

The weighted total degree with unit weight equals the ordinary total degree: for any polynomial φ, weightedTotalDegree(identity)(φ) = totalDegree(φ).

Русский

Взвешенная суммарная степень при весе равном единице совпадает с обычной степенью: weightedTotalDegree(1)(φ) = totalDegree(φ).

LaTeX

$$$\\operatorname{weightedTotalDegree}(1, \\varphi) = \\operatorname{totalDegree}(\\varphi)$$$

Lean4

theorem weightedTotalDegree_one (φ : MvPolynomial σ R) : weightedTotalDegree (1 : σ → ℕ) φ = φ.totalDegree := by
  simp only [totalDegree, weightedTotalDegree, weight, LinearMap.toAddMonoidHom_coe, linearCombination, Pi.one_apply,
    Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id, Algebra.id.smul_eq_mul, mul_one]

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