pow — Mathlib

English

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

Русский

Если φ однороден степени m, то φ^n однороден степени m·n.

LaTeX

$$(IsHomogeneous(\phi, m)) \Rightarrow IsHomogeneous(\phi^n, m * n)$$

Lean4

theorem pow (hφ : φ.IsHomogeneous m) (n : ℕ) : (φ ^ n).IsHomogeneous (m * n) :=
  by
  rw [show φ ^ n = ∏ _i ∈ Finset.range n, φ by simp]
  rw [show m * n = ∑ _i ∈ Finset.range n, m by simp [mul_comm]]
  apply IsHomogeneous.prod _ _ _ (fun _ _ ↦ hφ)

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