Commit 2025-04-06 18:39 53e51368

View on Github →

feat(NumberTheory): p-adic cyclotomic character (#21934)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem MulSemiringAction.toRingEquiv_algEquiv

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

added theorem CyclotomicCharacter.continuous

added theorem CyclotomicCharacter.spec

added theorem CyclotomicCharacter.toFun_apply

added theorem CyclotomicCharacter.toFun_spec

added theorem CyclotomicCharacter.toZModPow

added theorem CyclotomicCharacter.toZModPow_toFun

added theorem ModularCyclotomicCharacter.aux_spec

added theorem ModularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow

deleted theorem ModularCyclotomicCharacter_aux_spec

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

added theorem PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub

added theorem PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem Continuous.of_coeHom_comp