Documentation Verification Report

Complex

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

Statistics

Metric	Count
Definitions `PadicAlgCl`, `instCoePadic`, `instRankOneNNRealV`, `nontriviallyNormedField`, `normedAlgebra`, `normedField`, `valued`, `PadicComplex`, `instRankOneNNRealV`, `nontriviallyNormedField`, `normedField`, `valued`, `PadicComplexInt`, `«termℂ_[_]»`, `«term𝓞_ℂ_[_]»`	15
Theorems `charZero`, `coe_eq`, `instUniformContinuousConstSMulPadic`, `isAlgebraic`, `isNonarchimedean`, `isUltrametricDist`, `norm_extends`, `spectralNorm_eq`, `valuation_coe`, `valuation_def`, `valuation_p`, `hom_eq_embedding`, `charZero`, `coe_eq`, `coe_natCast`, `coe_zero`, `instIsScalarTowerPadicPadicAlgCl`, `isAlgClosed`, `isNonarchimedean`, `isUltrametricDist`, `nnnorm_extends`, `nnnorm_extends'`, `norm_eq_norm`, `norm_eq_norm'`, `norm_extends`, `norm_extends'`, `valuation_extends`, `valuation_p`, `integers`	29
Total	44

PadicAlgCl

Definitions

Name	Category	Theorems
`instCoePadic` 📖	CompOp	1 math math: `coe_eq`
`instRankOneNNRealV` 📖	CompOp	—
`nontriviallyNormedField` 📖	CompOp	—
`normedAlgebra` 📖	CompOp	—
`normedField` 📖	CompOp	27 math math: `PadicComplex.valuation_extends`, `PadicComplex.charZero`, `PadicComplex.coe_eq`, `PadicComplex.norm_eq_norm`, `PadicComplex.coe_natCast`, `isNonarchimedean`, `isUltrametricDist`, `norm_extends`, `instUniformContinuousConstSMulPadic`, `valuation_p`, `PadicComplex.valuation_p`, `spectralNorm_eq`, `PadicComplex.norm_extends'`, `PadicComplex.isNonarchimedean`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `PadicComplex.norm_eq_norm'`, `PadicComplex.isUltrametricDist`, `valuation_def`, `valuation_coe`, `PadicComplex.coe_zero`, `PadicComplex.RankOne.hom_eq_embedding`, `charZero`, `PadicComplex.norm_extends`, `PadicComplex.nnnorm_extends'`, `PadicComplex.nnnorm_extends`, `PadicComplexInt.integers`, `PadicComplex.isAlgClosed`
`valued` 📖	CompOp	21 math math: `PadicComplex.valuation_extends`, `PadicComplex.charZero`, `PadicComplex.coe_eq`, `PadicComplex.norm_eq_norm`, `PadicComplex.coe_natCast`, `instUniformContinuousConstSMulPadic`, `valuation_p`, `PadicComplex.valuation_p`, `PadicComplex.norm_extends'`, `PadicComplex.isNonarchimedean`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `PadicComplex.norm_eq_norm'`, `valuation_def`, `valuation_coe`, `PadicComplex.coe_zero`, `PadicComplex.RankOne.hom_eq_embedding`, `PadicComplex.norm_extends`, `PadicComplex.nnnorm_extends'`, `PadicComplex.nnnorm_extends`, `PadicComplexInt.integers`, `PadicComplex.isAlgClosed`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charZero` 📖	mathematical	—	`CharZero` `PadicAlgCl` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `normedField`	—	`RingHom.charZero_iff` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Padic.instCharZero`
`coe_eq` 📖	mathematical	—	`Padic` `PadicAlgCl` `instCoePadic` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldPadic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `RingHom.instFunLike` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id`	—	—
`instUniformContinuousConstSMulPadic` 📖	mathematical	—	`UniformContinuousConstSMul` `Padic` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `valued` `AlgebraicClosure.instSMulOfIsScalarTower` `instFieldPadic` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Padic.normedField` `IsScalarTower.right` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id`	—	`uniformContinuousConstSMul_of_continuousConstSMul` `Valued.toIsUniformAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `Padic` `PadicAlgCl` `instCommRingPadic` `DivisionRing.toRing` `Field.toDivisionRing` `AlgebraicClosure.instField` `instFieldPadic` `AlgebraicClosure.instAlgebra` `CommRing.toCommSemiring` `Algebra.id`	—	`AlgebraicClosure.isAlgebraic`
`isNonarchimedean` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `PadicAlgCl` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `normedField` `Norm.norm` `NormedField.toNorm`	—	`isNonarchimedean_spectralNorm` `Padic.instIsUltrametricDist` `isAlgebraic`
`isUltrametricDist` 📖	mathematical	—	`IsUltrametricDist` `PadicAlgCl` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `normedField`	—	`IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm` `isNonarchimedean`
`norm_extends` 📖	mathematical	—	`Norm.norm` `PadicAlgCl` `NormedField.toNorm` `normedField` `DFunLike.coe` `RingHom` `Padic` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldPadic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `RingHom.instFunLike` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id` `Padic.instNorm`	—	`norm_algebraMap'` `NormedDivisionRing.to_normOneClass`
`spectralNorm_eq` 📖	mathematical	—	`spectralNorm` `Padic` `Padic.normedField` `PadicAlgCl` `AlgebraicClosure.instField` `instFieldPadic` `AlgebraicClosure.instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Algebra.id` `Norm.norm` `NormedField.toNorm` `normedField`	—	—
`valuation_coe` 📖	mathematical	—	`NNReal.toReal` `DFunLike.coe` `Valuation` `PadicAlgCl` `NNReal` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `normedField` `Valuation.instFunLike` `Valued.v` `valued` `Norm.norm` `NormedField.toNorm`	—	—
`valuation_def` 📖	mathematical	—	`DFunLike.coe` `Valuation` `PadicAlgCl` `NNReal` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `normedField` `Valuation.instFunLike` `Valued.v` `valued` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing`	—	—
`valuation_p` 📖	mathematical	—	`DFunLike.coe` `Valuation` `PadicAlgCl` `NNReal` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `normedField` `Valuation.instFunLike` `Valued.v` `valued` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NNReal.instDiv` `NNReal.instOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NNReal.instSemiring`	—	`map_natCast` `RingHom.instRingHomClass` `NNReal.eq` `valuation_coe` `norm_extends` `Padic.norm_p` `one_div` `NNReal.coe_inv` `NNReal.coe_natCast`

PadicComplex

Definitions

Name	Category	Theorems
`instRankOneNNRealV` 📖	CompOp	3 math math: `norm_eq_norm`, `norm_eq_norm'`, `RankOne.hom_eq_embedding`
`nontriviallyNormedField` 📖	CompOp	—
`normedField` 📖	CompOp	—
`valued` 📖	CompOp	6 math math: `valuation_extends`, `norm_eq_norm`, `valuation_p`, `norm_eq_norm'`, `RankOne.hom_eq_embedding`, `PadicComplexInt.integers`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charZero` 📖	mathematical	—	`CharZero` `PadicComplex` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `UniformSpace.Completion.ring` `PadicAlgCl` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `Valued.toUniformSpace` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.charZero_iff` `PadicAlgCl.instUniformContinuousConstSMulPadic` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Padic.instCharZero`
`coe_eq` 📖	mathematical	—	`UniformSpace.Completion.coe'` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `DFunLike.coe` `RingHom` `PadicComplex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AlgebraicClosure.instField` `Padic` `instFieldPadic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `UniformSpace.Completion.instField` `Valued.isTopologicalDivisionRing` `Field.toDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `algebraMap` `UniformSpace.Completion.algebra'` `AlgebraicClosure.instCommRing`	—	—
`coe_natCast` 📖	mathematical	—	`UniformSpace.Completion.coe'` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `PadicComplex` `UniformSpace.Completion.ring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valued.completable` `map_natCast` `RingHom.instRingHomClass` `coe_eq`
`coe_zero` 📖	mathematical	—	`UniformSpace.Completion.coe'` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `UniformSpace.Completion` `instZeroCompletion`	—	—
`instIsScalarTowerPadicPadicAlgCl` 📖	mathematical	—	`IsScalarTower` `Padic` `PadicAlgCl` `PadicComplex` `AlgebraicClosure.instSMulOfIsScalarTower` `instFieldPadic` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Padic.normedField` `IsScalarTower.right` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `UniformSpace.Completion.instSMul` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `Algebra.toSMul` `AlgebraicClosure.instField`	—	`IsScalarTower.of_algebraMap_eq` `Valued.toIsUniformAddGroup` `Valued.isTopologicalDivisionRing` `PadicAlgCl.instUniformContinuousConstSMulPadic`
`isAlgClosed` 📖	mathematical	—	`IsAlgClosed` `PadicComplex` `UniformSpace.Completion.instField` `PadicAlgCl` `AlgebraicClosure.instField` `Padic` `instFieldPadic` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `Valued.isTopologicalDivisionRing` `Field.toDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup`	—	`IsAlgClosed.of_denseRange` `UniformSpace.Completion.completeSpace` `charZero` `isUltrametricDist` `UniformSpace.Completion.denseRange_coe` `AlgebraicClosure.isAlgClosed`
`isNonarchimedean` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `PadicComplex` `instAddCompletion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Norm.norm` `UniformSpace.Completion.instNorm` `NormedField.toNorm`	—	`IsUltrametricDist.norm_add_le_max` `isUltrametricDist`
`isUltrametricDist` 📖	mathematical	—	`IsUltrametricDist` `PadicComplex` `UniformSpace.Completion.instDist` `PadicAlgCl` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField`	—	`IsUltrametricDist.of_normedAlgebra` `Padic.instIsUltrametricDist`
`nnnorm_extends` 📖	mathematical	—	`NNNorm.nnnorm` `UniformSpace.Completion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.Completion.instNormedCommRing` `UniformSpace.Completion.coe'`	—	`NNReal.eq` `norm_extends`
`nnnorm_extends'` 📖	mathematical	—	`NNNorm.nnnorm` `UniformSpace.Completion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.Completion.instNormedCommRing` `UniformSpace.Completion.coe'` `DFunLike.coe` `RingHom` `Padic` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldPadic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `RingHom.instFunLike` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id` `Padic.normedField`	—	`NNReal.eq` `UniformSpace.Completion.nnnorm_coe` `nnnorm_algebraMap'` `NormedDivisionRing.to_normOneClass`
`norm_eq_norm` 📖	mathematical	—	`Norm.norm` `PadicComplex` `UniformSpace.Completion.instNorm` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `NormedField.toNorm` `Valuation.norm` `UniformSpace.Completion.instField` `AlgebraicClosure.instField` `Padic` `instFieldPadic` `Valued.isTopologicalDivisionRing` `Field.toDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `Valued.v` `DivisionRing.toRing` `valued` `instRankOneNNRealV`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `norm_eq_norm'`
`norm_eq_norm'` 📖	mathematical	—	`Norm.norm` `PadicComplex` `UniformSpace.Completion.instNorm` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `NormedField.toNorm` `Valuation.norm` `UniformSpace.Completion.instField` `AlgebraicClosure.instField` `Padic` `instFieldPadic` `Valued.isTopologicalDivisionRing` `Field.toDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `Valued.v` `DivisionRing.toRing` `valued` `instRankOneNNRealV`	—	`UniformSpace.Completion.extension_unique` `T3Space.toT0Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `instOrderTopologyReal` `Real.instCompleteSpace` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `uniformContinuous_norm` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `IsTopologicalDivisionRing.toIsTopologicalRing` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.norm_def` `Valuation.embedding_restrict` `valuation_extends` `PadicAlgCl.valuation_coe`
`norm_extends` 📖	mathematical	—	`Norm.norm` `UniformSpace.Completion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `UniformSpace.Completion.instNorm` `NormedField.toNorm` `UniformSpace.Completion.coe'`	—	`UniformSpace.Completion.norm_coe`
`norm_extends'` 📖	mathematical	—	`Norm.norm` `UniformSpace.Completion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `UniformSpace.Completion.instNorm` `NormedField.toNorm` `UniformSpace.Completion.coe'` `DFunLike.coe` `RingHom` `Padic` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldPadic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `RingHom.instFunLike` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id` `Padic.instNorm`	—	`UniformSpace.Completion.norm_coe` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass`
`valuation_extends` 📖	mathematical	—	`DFunLike.coe` `Valuation` `UniformSpace.Completion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `UniformSpace.Completion.ring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valuation.instFunLike` `Valued.v` `valued` `UniformSpace.Completion.coe'`	—	`Valued.extensionValuation_apply_coe`
`valuation_p` 📖	mathematical	—	`DFunLike.coe` `Valuation` `PadicComplex` `NNReal` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `UniformSpace.Completion.ring` `PadicAlgCl` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `Valued.toUniformSpace` `PadicAlgCl.valued` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valuation.instFunLike` `Valued.v` `valued` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NNReal.instDiv` `NNReal.instOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NNReal.instSemiring`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valued.completable` `map_natCast` `RingHom.instRingHomClass` `coe_eq` `valuation_extends` `PadicAlgCl.valuation_p`

PadicComplex.RankOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_eq_embedding` 📖	mathematical	—	`Valuation.RankOne.hom` `PadicComplex` `NNReal` `UniformSpace.Completion.ring` `PadicAlgCl` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `Valued.toUniformSpace` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valued.v` `PadicComplex.valued` `PadicComplex.instRankOneNNRealV` `MonoidWithZeroHom.ValueGroup₀.embedding` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `NNReal.instSemifield` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`

PadicComplexInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integers` 📖	mathematical	—	`Valuation.Integers` `PadicComplex` `NNReal` `UniformSpace.Completion.commRing` `PadicAlgCl` `AlgebraicClosure.instCommRing` `Padic` `instFieldPadic` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `Valued.toIsUniformAddGroup` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.v` `UniformSpace.Completion.ring` `PadicComplex.valued` `ValuationSubring` `UniformSpace.Completion.instField` `AlgebraicClosure.instField` `Field.toDivisionRing` `Valued.completable` `SetLike.instMembership` `ValuationSubring.instSetLike` `PadicComplexInt` `ValuationSubring.instCommRingSubtypeMem` `ValuationSubring.instAlgebraSubtypeMem`	—	`Valuation.integer.integers` `Valued.toIsUniformAddGroup` `IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing`

(root)

Definitions

Name	Category	Theorems
`PadicAlgCl` 📖	CompOp	29 math math: `PadicComplex.valuation_extends`, `PadicComplex.charZero`, `PadicComplex.coe_eq`, `PadicComplex.norm_eq_norm`, `PadicComplex.coe_natCast`, `PadicAlgCl.isNonarchimedean`, `PadicAlgCl.isUltrametricDist`, `PadicAlgCl.norm_extends`, `PadicAlgCl.instUniformContinuousConstSMulPadic`, `PadicAlgCl.valuation_p`, `PadicComplex.valuation_p`, `PadicAlgCl.spectralNorm_eq`, `PadicComplex.norm_extends'`, `PadicComplex.isNonarchimedean`, `PadicAlgCl.isAlgebraic`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `PadicComplex.norm_eq_norm'`, `PadicComplex.isUltrametricDist`, `PadicAlgCl.valuation_def`, `PadicAlgCl.valuation_coe`, `PadicComplex.coe_zero`, `PadicComplex.RankOne.hom_eq_embedding`, `PadicAlgCl.charZero`, `PadicComplex.norm_extends`, `PadicAlgCl.coe_eq`, `PadicComplex.nnnorm_extends'`, `PadicComplex.nnnorm_extends`, `PadicComplexInt.integers`, `PadicComplex.isAlgClosed`
`PadicComplex` 📖	CompOp	12 math math: `PadicComplex.charZero`, `PadicComplex.coe_eq`, `PadicComplex.norm_eq_norm`, `PadicComplex.coe_natCast`, `PadicComplex.valuation_p`, `PadicComplex.isNonarchimedean`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `PadicComplex.norm_eq_norm'`, `PadicComplex.isUltrametricDist`, `PadicComplex.RankOne.hom_eq_embedding`, `PadicComplexInt.integers`, `PadicComplex.isAlgClosed`
`PadicComplexInt` 📖	CompOp	1 math math: `PadicComplexInt.integers`
`«termℂ_[_]»` 📖	CompOp	—
`«term𝓞_ℂ_[_]»` 📖	CompOp	—

---

← Back to Index