Commit 2024-12-13 19:45 73ea8d5d
View on Github →feat(NumberTheory/Padics/RingHoms): add the equivalence between the residue field of Z_p and ZMod p (#19922)
We construct the equivalence between the residue field of Z_p and ZMod p in terms of the IsLocalRing.ResidueField declaration.