Commit 2026-08-27 09:46 900e11b0

View on Github →

feat(NumberTheory/Padics): the Amice transform (#42832) Prove the Amice (aka Leopoldt) transform isomorphism, identifying Zp-valued measures on Zp with the power series ring ℤ_[p]⟦X⟧.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/ForwardDiff.lean

modified theorem fwdDiff_choose

Modified Mathlib/NumberTheory/Padics/MahlerBasis.lean

added theorem PadicInt.dense_span_mahler

added theorem PadicInt.ext_mahler

Created Mathlib/NumberTheory/Padics/Measure/AmiceTransform.lean

added def AbstractMeasure.amiceTransform

added def AbstractMeasure.amiceTransformEquiv

added theorem AbstractMeasure.amiceTransformEquiv_apply

added theorem AbstractMeasure.amiceTransform_invTransform

added theorem AbstractMeasure.coeff_amiceTransform

added theorem AbstractMeasure.coeff_amiceTransformEquiv

added theorem AbstractMeasure.ext_mahler

added theorem AbstractMeasure.injective_amiceTransform

added def AbstractMeasure.invTransform

added theorem AbstractMeasure.invTransform_apply

Modified Mathlib/NumberTheory/Padics/Measure/Basic.lean

added def AbstractMeasure.arrowCongrLeft

added theorem AbstractMeasure.arrowCongrLeft_apply

added theorem AbstractMeasure.arrowCongrLeft_symm

added theorem AbstractMeasure.coe_arrowCongrLeft