Commit 2025-03-31 15:12 c6cd01be

View on Github →

feat(NumberTheory/Padics): Use NormMulClass for p-adic ints (#23348) Define an instance of NormMulClass on Z_[p].

Estimated changes

deleted theorem PadicInt.norm_mul
deleted theorem PadicInt.norm_pow