Theorems · Definition · number theory

PadicInt.limNthHom

{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 → ℤ_[p]

limNthHom f_compat r is the limit of a sequence f of compatible ring homs R →+* ZMod (p^k). This is itself a ring hom: see PadicInt.lift.

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

8 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringFact