Theorem AddChar.tendsto_eval_one_sub_pow

Modification history

2025-04-23 11:46
Mathlib/NumberTheory/Padics/AddChar.lean
feat(NumberTheory/Padics): leftovers from PR 24141 (#24310) …
Added AddChar.tendsto_eval_one_sub_powView on Github →