digits_eq_nil_iff_eq_zero — Mathlib

English

Digits in base b vanish only when the number is zero; i.e., digits_b n = [] if and only if n = 0.

Русский

Цифры в основании b распадаются в пустой список тогда и только тогда, когда число равно нулю.

LaTeX

$$$\\operatorname{digits}_b n = [] \\iff n = 0.$$$

Lean4

theorem digits_eq_nil_iff_eq_zero {b n : ℕ} : digits b n = [] ↔ n = 0 :=
  by
  constructor
  · intro h
    have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
    convert this
    rw [ofDigits_digits]
  · rintro rfl
    simp

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