Theorems · Theorem · order theory

IsNonarchimedean.apply_natCast_le_one

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3}
  [inst_2 : AddMonoidWithOne α] [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [OneHomClass F α R]
  {f : F}, IsNonarchimedean ⇑f → ∀ {n : ℕ}, f ↑n ≤ 1

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

3 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext

Assumes

SemiringLinearOrderAddMonoidWithOneFunLikeZeroHomClassNonnegHomClassOneHomClass