isCauSeq_nthHom — Mathlib

English

Each nthHom f r n equals the integer representative of f n r in ZMod(p^n).

Русский

Каждый nthHom f r n равен целочисленному представительному элементу f n r в ZMod(p^n).

LaTeX

$$nthHom f r n = (f n r).val$$

Lean4

theorem isCauSeq_nthHom (r : R) : IsCauSeq (padicNorm p) fun n => nthHom f r n :=
  by
  intro ε hε
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (p : ℚ) ^ (-((k : ℕ) : ℤ)) < ε := exists_pow_neg_lt_rat p hε
  use k
  intro j hj
  refine lt_of_le_of_lt ?_ hk
  beta_reduce
  norm_cast
  rw [← padicNorm.dvd_iff_norm_le]
  exact mod_cast pow_dvd_nthHom_sub f_compat r k j hj

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