ofDigits_lt_base_pow_length — Mathlib

English

For any b and m, m < (b+2)^{(digits(b+2,m)).length}.

Русский

Для любых b,m выполнено m < (b+2)^{(digits(b+2,m)).length}.

LaTeX

$$$ m < (b+2)^{\, (\mathrm{digits}(b+2,m)).length } $$$

Lean4

/-- an n-digit number in base b is less than b^n if b > 1 -/
theorem ofDigits_lt_base_pow_length {b : ℕ} {l : List ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) :
    ofDigits b l < b ^ l.length := by
  rcases b with (_ | _ | b) <;> try simp_all
  exact ofDigits_lt_base_pow_length' hl

Похожие утверждения