head and Nat.ofDigits/Nat.digits

Stream: mathlib4

[Moritz Firsching]

I needed the following two lemmas and was wondering if they would make a good contribution to mathlib. (I expected them to be there already, hopefully I didn't overlook them). What do you think?

theorem Nat.ofDigits_modEq_head (b : ℕ) (l : List ℕ) : (Nat.ofDigits b l) ≡ l.head! [ZMOD b] := by
  induction l
  · rfl
  · simp [Nat.ofDigits, Int.ModEq]

theorem Nat.digits_head {b n : ℕ} (hb : 1 < b): (Nat.digits b n).head! = n % b := by
  rcases n with _ | n
  · simp only [Nat.zero_eq, Nat.digits_zero, Nat.zero_mod]
    rfl
  · nth_rw 2 [← Nat.ofDigits_digits b n.succ]
    zify
    rw [Int.ModEq.eq <| Nat.ofDigits_modEq_head _ _]
    norm_cast
    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

[Kim Morrison]

Second one seems fine. I'm less keen of the ZMOD in the first one.

[Ruben Van de Velde]

There's a few lemmas about ofDigits with zmod already, fwiw

[Moritz Firsching]

I suppose

theorem Nat.ofDigits_modEq_head (b : ℕ) (l : List ℕ) : (Nat.ofDigits b l) % b = l.head! % b :=

might also be useful instead of the ZMOD version. At least this is exactly what I use in the proof of Nat.digits_head

[Moritz Firsching]

https://github.com/leanprover-community/mathlib4/pull/11129