ℚ machinery

theorem Rat.abs_eq_div {x : ℚ} : |x| = ↑x.num.natAbs / ↑x.den

theorem Rat.abs_eq_div' {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x : ℚ} : |↑x| = ↑x.num.natAbs / ↑x.den

@[irreducible]

def Rat.log2 (x : ℚ) : ℤ

n s.t. 2^n ≤ |x| < 2^(n+1) if n ≠ 0

Equations

• One or more equations did not get rendered due to their size.

theorem Rat.log2_correct {x : ℚ} (x0 : x ≠ 0) : |x| ∈ Set.Ico (2 ^ x.log2) (2 ^ (x.log2 + 1))

theorem Rat.log2_self_le {x : ℚ} (x0 : x ≠ 0) : 2 ^ x.log2 ≤ |x|

theorem Rat.lt_log2_self {x : ℚ} : |x| < 2 ^ (x.log2 + 1)