dvd_appr_sub_appr — Mathlib

English

If m ≤ n, then p^m divides appr(x,n) − appr(x,m).

Русский

Если m ≤ n, то p^m делит apr(x,n) − apr(x,m).

LaTeX

$$$p^m \mid \operatorname{appr}(x,n) - \operatorname{appr}(x,m) \quad (m \le n)$$$

Lean4

theorem dvd_appr_sub_appr (x : ℤ_[p]) (m n : ℕ) (h : m ≤ n) : p ^ m ∣ x.appr n - x.appr m :=
  by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h; clear h
  induction k with
  | zero => simp only [add_zero, le_refl, tsub_eq_zero_of_le, dvd_zero]
  | succ k ih =>
    rw [← add_assoc]
    dsimp [appr]
    split_ifs with h
    · exact ih
    rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
    apply dvd_add _ ih
    apply dvd_mul_of_dvd_left
    apply pow_dvd_pow _ (Nat.le_add_right m k)

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