ofDigits_inj_of_len_eq — Mathlib

English

If base b > 1 and two digit lists L1, L2 have the same length and every element is < b, and the resulting numbers are equal, then L1 = L2.

Русский

Пусть b > 1 и две цифрированные последовательности L1, L2 имеют одинаковую длину и все элементы меньше b; если ofDigits(b,L1) = ofDigits(b,L2), то L1 = L2.

LaTeX

$$$ \\text{If } hb:1

Lean4

theorem ofDigits_inj_of_len_eq {b : ℕ} (hb : 1 < b) {L1 L2 : List ℕ} (len : L1.length = L2.length)
    (w1 : ∀ l ∈ L1, l < b) (w2 : ∀ l ∈ L2, l < b) (h : ofDigits b L1 = ofDigits b L2) : L1 = L2 :=
  by
  induction L1 generalizing L2 with
  | nil =>
    simp only [List.length_nil] at len
    exact (List.length_eq_zero_iff.mp len.symm).symm
  | cons D L ih => ?_
  obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm
  simp only [List.length_cons, add_left_inj] at len
  simp only [ofDigits_cons] at h
  have eqd : D = d := by
    have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]
    simpa [mod_eq_of_lt (w2 d List.mem_cons_self), mod_eq_of_lt (w1 D List.mem_cons_self)] using H
  simp only [eqd, add_right_inj, mul_left_cancel_iff_of_pos (zero_lt_of_lt hb)] at h
  have := ih len (fun a ha ↦ w1 a <| List.mem_cons_of_mem D ha) (fun a ha ↦ w2 a <| List.mem_cons_of_mem d ha) h
  rw [eqd, this]

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