Mathlib Map

Theorems · Definition · number theory

PadicInt.zmodRepr

{p : ℕ} → [hp_prime : Fact (Nat.Prime p)] → ℤ_[p] → ℕ

zmodRepr x is the unique natural number smaller than p satisfying ‖(x - zmodRepr x : ℤ_[p])‖ < 1.

Defined in
Mathlib.NumberTheory.Padics.RingHoms
Cited by
21 results in Mathlib
Foundations
Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Fact
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PadicInt.toZMod · cited by 10PadicInt.toZModPadicInt.zmodRepr_unique · cited by 4PadicInt.zmodRepr_uniquePadicInt.zmodRepr_spec · cited by 3PadicInt.zmodRepr_specPadicInt.sub_zmodRepr_mem · cited by 3PadicInt.sub_zmodRepr_memPadicInt.toZMod_spec · cited by 3PadicInt.toZMod_specPadicInt.zmodRepr_eq_zero_iff_dvd · cited by 2PadicInt.zmodRepr_eq_zero…PadicInt.zmodRepr_eq_zero_of_dvd · cited by 2PadicInt.zmodRepr_eq_zero…PadicInt.zmodRepr_lt_p · cited by 2PadicInt.zmodRepr_lt_pPadicInt.norm_sub_zmodRepr_lt_one · cited by 2PadicInt.norm_sub_zmodRep…PadicInt.zmodRepr_natCast · cited by 1PadicInt.zmodRepr_natCastPadicInt.zmodRepr_natCast_of_lt · cited by 1PadicInt.zmodRepr_natCast…PadicInt.zmodRepr_zero · cited by 1PadicInt.zmodRepr_zeroPadicInt.norm_natCast_zmodRepr_eq · cited by 1PadicInt.norm_natCast_zmo…PadicInt.norm_natCast_zmodRepr_eq_one_iff · cited by 1PadicInt.norm_natCast_zmo…PadicInt.val_toZMod_eq_zmodRepr · cited by 0PadicInt.val_toZMod_eq_zm…Fact · cited by 2726FactNat.Prime · cited by 2059Nat.PrimePadicInt · cited by 179PadicIntPadicInt.zmodReprCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Factstatement and proof · cited by 2,726
  • Nat.Primestatement and proof · cited by 2,059
  • PadicIntstatement and proof · cited by 179

Cited by22

Results whose statement or proof uses this declaration.