le_coeffsIn_pow — Mathlib

English

For all n ≥ 0, there is a natural monotone relation between coeffsIn under HPow: coeffsIn(σ,M)^n ≤ coeffsIn(σ, M^n).

Русский

Для всех n ≥ 0 выполняется монотонное неравенство: coeffsIn(σ,M)^n ≤ coeffsIn(σ, M^n).

LaTeX

$$$\\forall n \\,(n \\ge 0) \\; \\text{we have } \\operatorname{coeffsIn}(\\sigma, M)^{n} \\le \\operatorname{coeffsIn}(\\sigma, M^{n})$$$

Lean4

theorem le_coeffsIn_pow : ∀ {n}, coeffsIn σ M ^ n ≤ coeffsIn σ (M ^ n)
  | 0 => by simpa using ⟨1, map_one _⟩
  | n + 1 => (coeffsIn_pow n.succ_ne_zero _).ge

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