Theorems · Theorem · number theory

PadicInt.lift_unique

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

One part of the universal property of ℤ_[p] as a projective limit. See also PadicInt.lift_spec.

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringFact