Theorems · Definition · number theory

PadicInt.nthHomSeq

{R : Type u_1} →
  [inst : NonAssocSemiring R] →
    {p : ℕ} →
      {f : (k : ℕ) → R →+* ZMod (p ^ k)} →
        [hp_prime : Fact (Nat.Prime p)] →
          (∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) → R → PadicSeq p

nthHomSeq f_compat r bundles PadicInt.nthHom f r as a Cauchy sequence of rationals with respect to the p-adic norm. The nth value of the sequence is ((f n r).val : ℚ).

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

4 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonAssocSemiringFact