Theorems · Theorem · order theory

IsNonarchimedean.apply_intCast_le_one

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3}
  [inst_3 : AddGroupWithOne α] [inst_4 : FunLike F α R] [AddGroupSeminormClass F α R] [OneHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {n : ℤ}, f ↑n ≤ 1

If f is a nonarchimedean additive group seminorm on α with f 1 = 1, then for every n : ℤ we have f n ≤ 1.

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringLinearOrderIsStrictOrderedRingAddGroupWithOneFunLikeAddGroupSeminormClassOneHomClass