pow — Mathlib

English

If φ is weighted homogeneous of degree m, then φ^n is weighted homogeneous of degree n·m.

Русский

Если полином взвешенно однороден степени m, то его n-я степень взвешенно однородна степени n·m.

LaTeX

$$IsWeightedHomogeneous w φ m → IsWeightedHomogeneous w (φ^n) (n • m)$$

Lean4

theorem pow {w : σ → M} (hφ : IsWeightedHomogeneous w φ m) (n : ℕ) : IsWeightedHomogeneous w (φ ^ n) (n • m) := by
  induction n with
  | zero => rw [pow_zero, zero_smul]; exact isWeightedHomogeneous_one R w
  | succ n ih => rw [pow_succ, succ_nsmul]; exact ih.mul hφ

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