Documentation Verification Report

MahlerBasis

📁 Source: Mathlib/NumberTheory/Padics/MahlerBasis.lean

Statistics

Metric	Count
Definitions `instBinomialRing`, `mahlerEquiv`, `mahlerSeries`, `mahlerTerm`, `mahler`	5
Theorems `norm_fwdDiff_iter_apply_le`, `continuous_choose`, `continuous_multichoose`, `fwdDiff_iter_le_of_forall_le`, `fwdDiff_mahlerSeries`, `fwdDiff_tendsto_zero`, `hasSum_mahler`, `hasSum_mahlerSeries`, `instIsAddTorsionFree`, `mahlerEquiv_apply`, `mahlerEquiv_symm_apply`, `mahlerSeries_apply`, `mahlerSeries_apply_nat`, `mahlerTerm_apply`, `mahlerTerm_one`, `norm_ascPochhammer_le`, `norm_mahlerTerm`, `norm_mahler_eq`, `mahler_apply`, `mahler_natCast_eq`	20
Total	25

IsUltrametricDist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_fwdDiff_iter_apply_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Nat.iterate` `fwdDiff` `SeminormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMap.instFunLike` `ContinuousMap.instNorm`	—	`fwdDiff_iter_eq_sum_shift` `norm_sum_le_of_forall_le_of_nonneg` `norm_nonneg` `LE.le.trans` `norm_zsmul_le` `ContinuousMap.norm_coe_le_norm`

PadicInt

Definitions

Name	Category	Theorems
`instBinomialRing` 📖	CompOp	3 math math: `continuous_choose`, `continuous_multichoose`, `mahler_apply`
`mahlerEquiv` 📖	CompOp	2 math math: `mahlerEquiv_apply`, `mahlerEquiv_symm_apply`
`mahlerSeries` 📖	CompOp	6 math math: `mahlerSeries_apply`, `coe_addChar_of_value_at_one`, `mahlerSeries_apply_nat`, `hasSum_mahlerSeries`, `fwdDiff_mahlerSeries`, `mahlerEquiv_symm_apply`
`mahlerTerm` 📖	CompOp	5 math math: `norm_mahlerTerm`, `mahlerTerm_apply`, `mahlerTerm_one`, `hasSum_mahlerSeries`, `hasSum_mahler`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_choose` 📖	mathematical	—	`Continuous` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `Ring.choose` `NonAssocRing.toAddCommGroupWithOne` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instBinomialRing`	—	`Continuous.comp'` `continuous_multichoose` `Continuous.fun_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `instIsUltrametricDist` `continuous_id'` `continuous_const`
`continuous_multichoose` 📖	mathematical	—	`Continuous` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `Ring.multichoose` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `instBinomialRing`	—	`Continuous.comp'` `Continuous.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_id'` `continuous_subtype_val` `Polynomial.continuous` `NonUnitalSeminormedRing.toIsTopologicalRing`
`fwdDiff_iter_le_of_forall_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instFunLike` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `ContinuousMap.instNorm` `compactSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast`	`Nat.iterate` `fwdDiff` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Nat.instMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`compactSpace` `MulZeroClass.zero_mul` `add_zero` `pow_zero` `div_one` `IsUltrametricDist.norm_fwdDiff_iter_apply_le` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_assoc` `LE.le.trans` `max_le` `coe_nnnorm` `NNReal.coe_natCast` `NNReal.coe_pow` `NNReal.coe_div` `NNReal.coe_le_coe` `Finset.sup_le` `pow_succ` `div_div` `div_le_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `NNReal.instIsStrictOrderedRing` `Nat.cast_zero` `NNReal.addLeftMono` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Nat.Prime.pos` `Fact.out` `add_right_comm` `Nat.cast_one` `div_le_div_of_nonneg_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `pow_le_pow_right₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.Prime.one_le` `le_rfl`
`fwdDiff_mahlerSeries` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Nat.iterate` `fwdDiff` `PadicInt` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `mahlerSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`fwdDiff_iter_eq_sum_shift` `Finset.sum_congr` `zero_add` `nsmul_one` `mahlerSeries_apply_nat` `Finset.mem_range` `Nat.cast_id` `Finset.smul_sum` `Finset.sum_comm` `Finset.sum_smul` `smul_assoc` `AddCommGroup.intIsScalarTower` `natCast_zsmul` `fwdDiff_iter_choose_zero` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`
`fwdDiff_tendsto_zero` 📖	mathematical	—	`Filter.Tendsto` `Nat.iterate` `fwdDiff` `PadicInt` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `ContinuousMap` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Filter.atTop` `Nat.instPreorder` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`NormedAddCommGroup.tendsto_nhds_zero` `compactSpace` `Filter.Tendsto.div_atTop` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_const_nhds` `tendsto_pow_atTop_atTop_of_one_lt` `AddGroup.existsAddOfLE` `Real.instArchimedean` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Nat.Prime.one_lt` `Fact.out` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually_lt_const` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.Eventually.mp` `eq_or_ne` `zpow_neg` `zpow_natCast` `sub_self` `norm_zero` `zero_div` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `norm_pos_iff` `Nat.cast_zero` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.Prime.pos` `ContinuousMap.uniform_continuity` `exists_pow_neg_lt` `dist_eq_norm_sub` `LT.lt.le` `LE.le.trans_lt` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `fwdDiff_iter_le_of_forall_le` `Filter.Eventually.of_forall` `lt_of_le_of_lt`
`hasSum_mahler` 📖	mathematical	—	`HasSum` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `ContinuousMap.compactOpen` `mahlerTerm` `Nat.iterate` `fwdDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `ContinuousMap.instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `hasSum_mahlerSeries` `fwdDiff_tendsto_zero` `ContinuousMap.coe_injective` `DenseRange.equalizer` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `denseRange_natCast` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `mahlerSeries_apply_nat` `le_rfl` `nsmul_eq_mul` `mul_one` `zero_add` `shift_eq_sum_fwdDiff_iter`
`hasSum_mahlerSeries` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`HasSum` `ContinuousMap` `PadicInt` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `ContinuousMap.compactOpen` `mahlerTerm` `mahlerSeries` `SummationFilter.unconditional`	—	`Summable.hasSum` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero` `SeminormedAddCommGroup.to_isUniformAddGroup` `compactSpace` `ContinuousMap.isUltrametricDist` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `CompactlyCoherentSpace.of_sequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `tendsto_zero_iff_norm_tendsto_zero` `norm_mahlerTerm` `Nat.cofinite_eq_atTop`
`instIsAddTorsionFree` 📖	mathematical	—	`IsAddTorsionFree` `PadicInt` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`smul_right_injective` `IsAddTorsionFree.to_isTorsionFree_nat` `IsAddTorsionFree.of_isCancelMulZero_charZero` `instCharZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Nat.instIsCancelMulZero`
`mahlerEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instTopologicalSpaceNat` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ZeroAtInftyContinuousMap.instFunLike` `LinearIsometryEquiv` `PadicInt` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMap` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ContinuousMap.instSeminormedAddCommGroup` `compactSpace` `ZeroAtInftyContinuousMap.instSeminormedAddCommGroup` `ContinuousMap.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ZeroAtInftyContinuousMap.instModule` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `mahlerEquiv` `Nat.iterate` `fwdDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousMap.instFunLike`	—	`RingHomInvPair.ids` `compactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`mahlerEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `PadicInt` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ZeroAtInftyContinuousMap` `instTopologicalSpaceNat` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ZeroAtInftyContinuousMap.instSeminormedAddCommGroup` `ContinuousMap.instSeminormedAddCommGroup` `compactSpace` `ZeroAtInftyContinuousMap.instModule` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ContinuousMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `mahlerEquiv` `mahlerSeries` `ZeroAtInftyContinuousMap.instFunLike`	—	`RingHomInvPair.ids` `compactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`mahlerSeries_apply` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DFunLike.coe` `ContinuousMap` `PadicInt` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ContinuousMap.instFunLike` `mahlerSeries` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Module.toDistribMulAction` `mahler` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `ContinuousMap.tsum_apply` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasSum.summable` `hasSum_mahlerSeries` `SummationFilter.instNeBotUnconditional` `mahlerTerm_apply`
`mahlerSeries_apply_nat` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DFunLike.coe` `ContinuousMap` `PadicInt` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ContinuousMap.instFunLike` `mahlerSeries` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Nat.choose`	—	`Nat.choose_eq_zero_of_lt` `zero_smul` `summable_zero` `mahlerSeries_apply` `mahler_natCast_eq` `Nat.cast_smul_eq_nsmul` `Summable.sum_add_tsum_nat_add'` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalAddGroup.toContinuousAdd` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `tsum_zero` `add_zero`
`mahlerTerm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instFunLike` `mahlerTerm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `mahler`	—	—
`mahlerTerm_one` 📖	mathematical	—	`mahlerTerm` `PadicInt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instNormedCommRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `NormSMulClass.toIsBoundedSMul` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Ring.toSemiring` `SeminormedRing.toRing` `NormMulClass.toNormSMulClass` `SeminormedRing.toNorm` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `instNormMulClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `mahler`	—	`ContinuousMap.ext` `NormSMulClass.toIsBoundedSMul` `NormMulClass.toNormSMulClass` `instNormMulClass` `mahlerTerm_apply` `mul_one`
`norm_ascPochhammer_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `PadicInt` `instNorm` `Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ascPochhammer` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `instNormedCommRing` `Nat.factorial`	—	`Nat.cast_ne_zero` `instCharZero` `Nat.factorial_ne_zero` `Polynomial.continuousAt` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Metric.continuousAt_iff` `norm_pos_iff` `DenseRange.exists_dist_lt` `denseRange_natCast` `LT.lt.le` `dist_comm` `LE.le.trans` `IsUltrametricDist.norm_add_le_max` `instIsUltrametricDist` `max_le` `Polynomial.eval_eq_smeval` `Nat.cast_mul` `norm_mul` `instNormMulClass` `mul_le_of_le_one_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `norm_le_one` `sub_add_cancel`
`norm_mahlerTerm` 📖	mathematical	—	`Norm.norm` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instNorm` `compactSpace` `mahlerTerm` `NormedAddCommGroup.toNorm`	—	`le_antisymm` `compactSpace` `ContinuousMap.norm_le_of_nonempty` `LE.le.trans` `norm_smul_le` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `norm_le_one` `le_trans` `mahlerTerm_apply` `mahler_natCast_eq` `Nat.choose_self` `Nat.cast_one` `one_smul` `ContinuousMap.norm_coe_le_norm`
`norm_mahler_eq` 📖	mathematical	—	`Norm.norm` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `ContinuousMap.instNorm` `compactSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `mahler` `Real` `Real.instOne`	—	`compactSpace` `NormSMulClass.toIsBoundedSMul` `NormMulClass.toNormSMulClass` `instNormMulClass` `norm_mahlerTerm` `NormOneClass.norm_one` `instNormOneClass`

(root)

Definitions

Name	Category	Theorems
`mahler` 📖	CompOp	6 math math: `PadicInt.mahlerTerm_apply`, `PadicInt.mahlerSeries_apply`, `mahler_natCast_eq`, `PadicInt.mahlerTerm_one`, `PadicInt.norm_mahler_eq`, `mahler_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mahler_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PadicInt.instNormedCommRing` `ContinuousMap.instFunLike` `mahler` `Ring.choose` `NonAssocRing.toAddCommGroupWithOne` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `PadicInt.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PadicInt.instBinomialRing`	—	—
`mahler_natCast_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PadicInt.instNormedCommRing` `ContinuousMap.instFunLike` `mahler` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Nat.choose`	—	`Ring.choose_natCast` `Monoid.PowAssoc`

---

← Back to Index