le_inf_support_pow — Mathlib

English

The infimum of the degree support of f^n is at least n times the infimum of the degree support of f.

Русский

Инфинум поддержки степеней для f^n не меньше n раз инфимума степени f.

LaTeX

$$$ (f^n)\\!\\text{support.inf deg} \\ge n \\cdot (f\\!\\text{support.inf deg})$$$

Lean4

theorem le_inf_support_pow (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (n : ℕ) (f : R[A]) :
    n • f.support.inf degt ≤ (f ^ n).support.inf degt :=
  by
  refine
    OrderDual.ofDual_le_ofDual.mpr <|
      sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_) (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f
  · exact degt0
  · exact degtm _ _

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