norm_zpow_le_mul_norm — Mathlib

English

For any a in a normed group and any integer n, ∥a^n∥ ≤ ∥n∥ · ∥a∥.

Русский

Для любого a в нормированной группе и целого n выполняется неравенство ∥a^n∥ ≤ ∥n∥ · ∥a∥.

LaTeX

$$$\|a^{n}\| \le \|n\| \cdot \|a\|$$$

Lean4

@[to_additive norm_zsmul_le]
theorem norm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖ := by
  rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa [Int.norm_natCast] using norm_pow_le_mul_norm

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