norm_pow_le — Mathlib

English

For a ∈ α and n ∈ ℕ, ‖a^n‖ ≤ ‖a‖^n when α has norm one.

Русский

Для a и n, при норме единицы, ‖a^n‖ ≤ ‖a‖^n.

LaTeX

$$$‖a^n‖ ≤ ‖a‖^n$ for all n ∈ ℕ.$$

Lean4

/-- If `α` is a seminormed ring with `‖1‖ = 1`, then `‖a ^ n‖ ≤ ‖a‖ ^ n`.
See also `norm_pow_le'`. -/
theorem norm_pow_le [NormOneClass α] (a : α) (n : ℕ) : ‖a ^ n‖ ≤ ‖a‖ ^ n :=
  Nat.recOn n (by simp only [pow_zero, norm_one, le_rfl]) fun n _hn => norm_pow_le' a n.succ_pos

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