Theorems · Theorem · order theory

IsNonarchimedean.add_pow_le

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : CommRing α]
  [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [SubmultiplicativeHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ (n : ℕ) (a b : α), ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

If f is a nonarchimedean additive group seminorm on a commutative ring α, n : ℕ, and a b : α, then we can find m : ℕ such that m ≤ n and f ((a + b) ^ n) ≤ (f (a ^ m)) * (f (b ^ (n - m))).

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

1 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringLinearOrderCommRingFunLikeZeroHomClassNonnegHomClassSubmultiplicativeHomClass