Theorems · Definition · number theory

Int.clogZPowGi

(R : Type u_1) →
  [inst : Semifield R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        [inst_3 : FloorSemiring R] →
          {b : ℕ} → (hb : 1 < b) → GaloisInsertion (fun r => Int.clog b ↑r) fun z => ⟨↑b ^ z, ⋯⟩

Over suitable subtypes, Int.clog and zpow form a Galois insertion

Defined in: Mathlib.Data.Int.Log
Cited by: 2 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semifield LinearOrder IsStrictOrderedRing FloorSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
LinearOrderstatement and proof · cited by 8,572
Set.Elemstatement · cited by 7,166
IsStrictOrderedRingstatement and proof · cited by 2,490
Nat.cast_zerostatement · cited by 1,870
Set.Ioistatement · cited by 1,463
zero_lt_onestatement · cited by 598
Semifieldstatement and proof · cited by 439
LT.lt.transstatement · cited by 370
FloorSemiringstatement and proof · cited by 179
GaloisInsertionstatement · cited by 35
zpow_posstatement · cited by 22

Cited by2

Results whose statement or proof uses this declaration.

Int.le_zpow_iff_clog_leproof · cited by 1
Int.zpow_lt_iff_lt_clogproof · cited by 0