Theorem AddChar.tendsto_apply_one_sub_pow

Modification history

2025-04-23 11:46
Mathlib/NumberTheory/Padics/AddChar.lean
feat(NumberTheory/Padics): leftovers from PR 24141 (#24310) …
Deleted AddChar.tendsto_apply_one_sub_powView on Github →
2025-04-23 09:35
Mathlib/NumberTheory/Padics/AddChar.lean
feat(NumberTheory/Padics): parametrization of cts add chars of Z_[p] (#24141) …
Added AddChar.tendsto_apply_one_sub_powView on Github →