Theorems · Definition · number theory

PadicInt.nthHom

{R : Type u_1} → [inst : NonAssocSemiring R] → {p : ℕ} → ((k : ℕ) → R →+* ZMod (p ^ k)) → R → ℕ → ℤ

Given a family of ring homs f : Π n : ℕ, R →+* ZMod (p ^ n), nthHom f r is an integer-valued sequence whose nth value is the unique integer k such that 0 ≤ k < p ^ n and f n r = (k : ZMod (p ^ n)).

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

10 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Quot.sound

Assumes

NonAssocSemiring