dvd_ofDigits_sub_ofDigits — Mathlib

English

If k divides a − b in a commutative ring, then k divides ofDigits a L − ofDigits b L for any list L of natural numbers.

Русский

Если k делит a − b в коммутативном кольце, то k делит ofDigits a L − ofDigits b L для любого списка L натуральных чисел.

LaTeX

$$$ k \mid a - b \; \Rightarrow \; k \mid \operatorname{ofDigits}(a,L) - \operatorname{ofDigits}(b,L) $ (для всех L).$$

Lean4

theorem dvd_ofDigits_sub_ofDigits {α : Type*} [CommRing α] {a b k : α} (h : k ∣ a - b) (L : List ℕ) :
    k ∣ ofDigits a L - ofDigits b L := by
  induction L with
  | nil => change k ∣ 0 - 0; simp
  | cons d L ih =>
    simp only [ofDigits, add_sub_add_left_eq_sub]
    exact dvd_mul_sub_mul h ih

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