totalDegree — Mathlib

English

If φ ≠ 0 and φ is homogeneous of degree n, then totalDegree φ = n.

Русский

Если φ ≠ 0 и φ однороден степени n, то общая степень φ равна n.

LaTeX

$$(IsHomogeneous(φ, n) \land φ \neq 0) → totalDegree(φ) = n$$

Lean4

theorem totalDegree (hφ : IsHomogeneous φ n) (h : φ ≠ 0) : totalDegree φ = n :=
  by
  apply le_antisymm hφ.totalDegree_le
  obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
  simp only [← hφ hd, MvPolynomial.totalDegree, Finsupp.sum]
  replace hd := Finsupp.mem_support_iff.mpr hd
  simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]
    -- Porting note: Original proof did not define `f`

  exact Finset.le_sup (f := fun s ↦ ∑ x ∈ s.support, s x) hd

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