head!_digits — Mathlib

English

If b ≠ 1, then the head of digits(b,n) equals n mod b.

Русский

Если b ≠ 1, то голова digits(b,n) равна n mod b.

LaTeX

$$$ (\mathrm{digits}(b,n)).head! = n \bmod b, \quad b \neq 1 $$$

Lean4

theorem head!_digits {b n : ℕ} (h : b ≠ 1) : (Nat.digits b n).head! = n % b :=
  by
  by_cases hb : 1 < b
  · rcases n with _ | n
    · simp
    · nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
      rw [Nat.ofDigits_mod_eq_head! _ _]
      exact
        (Nat.mod_eq_of_lt
            (Nat.digits_lt_base hb <|
              List.head!_mem_self <| Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm
  · rcases n with _ | _ <;> simp_all [show b = 0 by cutsat]

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