Theorems · Theorem · number theory

PadicInt.toZModPow_eq_iff_ext

∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [inst : NonAssocSemiring R] {g g' : R →+* ℤ_[p]},
  (∀ (n : ℕ), (PadicInt.toZModPow n).comp g = (PadicInt.toZModPow n).comp g') ↔ g = g'

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactNonAssocSemiring