Commit 2025-04-23 09:35 ee48509d

View on Github →

feat(NumberTheory/Padics): parametrization of cts add chars of Z_[p] (#24141) Another step towards defining the Mahler / Amice transform for p-adic measures.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/ForwardDiff.lean

added theorem fwdDiff_addChar_eq

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

added theorem tendsto_pow_atTop_nhds_zero_iff_norm_lt_one

modified theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one

Created Mathlib/NumberTheory/Padics/AddChar.lean

added theorem AddChar.tendsto_apply_one_sub_pow

added theorem PadicInt.addChar_of_value_at_one_def

added theorem PadicInt.coe_addChar_of_value_at_one

added theorem PadicInt.continuousAddCharEquiv_apply

added theorem PadicInt.continuousAddCharEquiv_of_norm_mul_apply

added theorem PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply

added theorem PadicInt.continuousAddCharEquiv_symm_apply

added theorem PadicInt.continuous_addChar_of_value_at_one

added theorem PadicInt.eq_addChar_of_value_at_one

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

added theorem DenseRange.addChar_eq_of_apply_one_eq