Commit 2025-04-23 11:46 e899d4c6

View on Github →

feat(NumberTheory/Padics): leftovers from PR 24141 (#24310) Rename some lemmas, add a TODO note

Estimated changes

Modified Mathlib/NumberTheory/Padics/AddChar.lean

deleted theorem AddChar.tendsto_apply_one_sub_pow

added theorem AddChar.tendsto_eval_one_sub_pow

Modified Mathlib/Topology/Algebra/Monoid/AddChar.lean

deleted theorem DenseRange.addChar_eq_of_apply_one_eq

added theorem DenseRange.addChar_eq_of_eval_one_eq