sup_support_pow_le — Mathlib

English

For a natural power f^n in the monoid algebra, the supremum of the degree is bounded by n times the supremum of the degree of f.

Русский

Для степени f^n в алгебре моноидов верхняя грань степени ограничена n-кратной верхней гранью степени f.

LaTeX

$$$ (f^n)\\!\\text{support.sup deg} ≤ n \\cdot (f\\!\\text{support.sup deg})$$$

Lean4

theorem sup_support_pow_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (n : ℕ) (f : R[A]) :
    (f ^ n).support.sup degb ≤ n • f.support.sup degb :=
  by
  rw [← List.prod_replicate, ← List.sum_replicate]
  refine (sup_support_list_prod_le degb0 degbm _).trans_eq ?_
  rw [List.map_replicate]

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