English
For any RingSeminorm p on a ring, and any nonzero natural exponent n, p(a^n) ≤ p(a)^n.
Русский
Для кольцевого семинормa p на кольце верно: для любого не нулевого натурального n выполняется p(a^n) ≤ p(a)^n.
LaTeX
$$$\forall {F α} [Ring α] [RingSeminormClass F α ℝ] (f : F) (a : α)\, \forall n : \mathbb{N},\ n \neq 0 \Rightarrow f(a^n) \le f(a)^n$$$
Lean4
/-- If `f` is a ring seminorm on `a`, then `∀ {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n`. -/
theorem map_pow_le_pow {F α : Type*} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] (f : F) (a : α) :
∀ {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n
| 0, h => absurd rfl h
| 1, _ => by simp only [pow_one, le_refl]
| n + 2, _ => by
simp only [pow_succ _ (n + 1)]
exact
le_trans (map_mul_le_mul f _ a)
(mul_le_mul_of_nonneg_right (map_pow_le_pow _ _ n.succ_ne_zero) (apply_nonneg f a))
