Commit 2025-08-25 03:00 73ce97e5

feat(NumberTheory/Padics): norm of Int lt one iff p divides (#27958) On the way to p-1 roots of unity With helper lemmas for natCast and simplification of norms of Int.natAbs Move some lemmas out of padicNormE namespace into Padic namespace which is similar to already existing lemmas in PadicInt namespace