digits_zero_of_eq_zero — Mathlib

English

If b ≠ 0 and the base-b value of a list L is zero, then every element of L equals zero.

Русский

Если b ≠ 0 и значение списка цифр L в основании b равно нулю, то каждый элемент списка равен нулю.

LaTeX

$$$\\forall b \\,(b \\neq 0) \\Rightarrow \\forall L\\; (\\operatorname{ofDigits}(b,L) = 0) \\Rightarrow \\forall l \\in L,\\; l = 0.$$$

Lean4

theorem digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) : ∀ {L : List ℕ} (_ : ofDigits b L = 0), ∀ l ∈ L, l = 0
  | _ :: _, h0, _, List.Mem.head .. => Nat.eq_zero_of_add_eq_zero_right h0
  | _ :: _, h0, _, List.Mem.tail _ hL =>
    digits_zero_of_eq_zero h (mul_right_injective₀ h (Nat.eq_zero_of_add_eq_zero_left h0)) _ hL

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