Theorem PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub

Modification history

2025-04-06 18:39
Mathlib/NumberTheory/Padics/RingHoms.lean
feat(NumberTheory): p-adic cyclotomic character (#21934)
Added PadicInt.isCauSeq_padicNorm_of_pow_dvd_subView on Github →