Theorems · Definition · number theory

PadicInt.lift

{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]

lift f_compat is the limit of a sequence f of compatible ring homs R →+* ZMod (p^k), with the equality lift f_compat r = PadicInt.limNthHom f_compat r.

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

6 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringFact