Theorems · Theorem · number theory

Int.zpow_lt_iff_lt_clog

∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (↑b ^ x < r ↔ x < Int.clog b r)

Int.clog b and zpow b (almost) form a Galois connection.

Defined in

Mathlib.Data.Int.Log

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingFloorSemiring