Documentation Verification Report

AddChar

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

Statistics

Metric	Count
Definitions `addChar_of_value_at_one`, `continuousAddCharEquiv`, `continuousAddCharEquiv_of_norm_mul`	3
Theorems `tendsto_eval_one_sub_pow`, `addChar_of_value_at_one_def`, `coe_addChar_of_value_at_one`, `continuousAddCharEquiv_apply`, `continuousAddCharEquiv_of_norm_mul_apply`, `continuousAddCharEquiv_of_norm_mul_symm_apply`, `continuousAddCharEquiv_symm_apply`, `continuous_addChar_of_value_at_one`, `eq_addChar_of_value_at_one`	9
Total	12

AddChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_eval_one_sub_pow` 📖	mathematical	`Continuous` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PadicInt.instNormedCommRing` `NormedRing.toSeminormedRing` `DFunLike.coe` `AddChar` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `instFunLike`	`Filter.Tendsto` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedCommRing.toNormedRing` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Filter.Tendsto.congr` `map_zero_eq_one` `mul_one` `fwdDiff_addChar_eq` `PadicInt.fwdDiff_tendsto_zero`

PadicInt

Definitions

Name	Category	Theorems
`addChar_of_value_at_one` 📖	CompOp	6 math math: `coe_addChar_of_value_at_one`, `eq_addChar_of_value_at_one`, `continuous_addChar_of_value_at_one`, `continuousAddCharEquiv_of_norm_mul_symm_apply`, `continuousAddCharEquiv_symm_apply`, `addChar_of_value_at_one_def`
`continuousAddCharEquiv` 📖	CompOp	2 math math: `continuousAddCharEquiv_symm_apply`, `continuousAddCharEquiv_apply`
`continuousAddCharEquiv_of_norm_mul` 📖	CompOp	2 math math: `continuousAddCharEquiv_of_norm_mul_apply`, `continuousAddCharEquiv_of_norm_mul_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addChar_of_value_at_one_def` 📖	mathematical	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`DFunLike.coe` `AddChar` `PadicInt` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddChar.instFunLike` `addChar_of_value_at_one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedCommRing.toNormedRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`mahlerSeries_apply_nat` `le_rfl` `Finset.sum_range_succ` `Finset.sum_range_one` `Nat.choose_zero_right` `Nat.choose_self` `one_smul` `pow_zero` `pow_one`
`coe_addChar_of_value_at_one` 📖	mathematical	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`DFunLike.coe` `AddChar` `PadicInt` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddChar.instFunLike` `addChar_of_value_at_one` `ContinuousMap` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedRing.toNonUnitalNormedRing` `ContinuousMap.instFunLike` `mahlerSeries` `Algebra.toModule` `CommRing.toCommSemiring` `instCommRing`	—	—
`continuousAddCharEquiv_apply` 📖	mathematical	`Continuous` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `NormedRing.toSeminormedRing` `DFunLike.coe` `AddChar` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `AddChar.instFunLike`	`Filter.Tendsto` `Monoid.toNatPow` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `continuousAddCharEquiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedCommRing.toNormedRing`	—	—
`continuousAddCharEquiv_of_norm_mul_apply` 📖	mathematical	`Continuous` `PadicInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `NormedRing.toSeminormedRing` `DFunLike.coe` `AddChar` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `AddChar.instFunLike`	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `continuousAddCharEquiv_of_norm_mul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedCommRing.toNormedRing`	—	—
`continuousAddCharEquiv_of_norm_mul_symm_apply` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`AddChar` `PadicInt` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Continuous` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedRing.toSeminormedRing` `DFunLike.coe` `AddChar.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `continuousAddCharEquiv_of_norm_mul` `addChar_of_value_at_one` `Filter.Tendsto` `Monoid.toNatPow` `SeminormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toNorm` `tendsto_pow_atTop_nhds_zero_iff_norm_lt_one`	—	—
`continuousAddCharEquiv_symm_apply` 📖	mathematical	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`AddChar` `PadicInt` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `instNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Continuous` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DFunLike.coe` `AddChar.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `continuousAddCharEquiv` `addChar_of_value_at_one`	—	—
`continuous_addChar_of_value_at_one` 📖	mathematical	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Continuous` `PadicInt` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `DFunLike.coe` `AddChar` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddChar.instFunLike` `addChar_of_value_at_one`	—	`ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass`
`eq_addChar_of_value_at_one` 📖	mathematical	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Continuous` `PadicInt` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instNormedCommRing` `DFunLike.coe` `AddChar` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddChar.instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedCommRing.toNormedRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	`addChar_of_value_at_one`	—	`DenseRange.addChar_eq_of_eval_one_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `denseRange_natCast` `continuous_addChar_of_value_at_one` `addChar_of_value_at_one_def`

---

← Back to Index