Documentation Verification Report

Complex

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

Statistics

Metric	Count
Definitions `PadicAlgCl`, `instCoePadic`, `instRankOneNNRealV`, `normedField`, `valued`, `PadicComplex`, `instAlgebraPadic`, `instNormedField`, `instRankOneNNRealV`, `valued`, `PadicComplexInt`, `«termℂ_[_]»`, `«term𝓞_ℂ_[_]»`	13
Theorems `coe_eq`, `instIsUltrametricDist`, `instUniformContinuousConstSMulPadic`, `isAlgebraic`, `isNonarchimedean`, `norm_extends`, `spectralNorm_eq`, `valuation_coe`, `valuation_def`, `valuation_p`, `coe_eq`, `coe_natCast`, `coe_zero`, `instIsScalarTowerPadicPadicAlgCl`, `isNonarchimedean`, `nnnorm_extends`, `norm_def`, `norm_extends`, `rankOne_hom_eq`, `valuation_extends`, `valuation_p`, `integers`	22
Total	35

PadicAlgCl

Definitions

Name	Category	Theorems
`instCoePadic` 📖	CompOp	1 math math: `coe_eq`
`instRankOneNNRealV` 📖	CompOp	1 math math: `PadicComplex.rankOne_hom_eq`
`normedField` 📖	CompOp	20 math math: `PadicComplex.valuation_extends`, `PadicComplex.coe_eq`, `PadicComplex.norm_def`, `PadicComplex.coe_natCast`, `isNonarchimedean`, `norm_extends`, `instUniformContinuousConstSMulPadic`, `valuation_p`, `PadicComplex.valuation_p`, `spectralNorm_eq`, `PadicComplex.isNonarchimedean`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `valuation_def`, `valuation_coe`, `PadicComplex.coe_zero`, `PadicComplex.norm_extends`, `PadicComplex.rankOne_hom_eq`, `instIsUltrametricDist`, `PadicComplex.nnnorm_extends`, `PadicComplexInt.integers`
`valued` 📖	CompOp	16 math math: `PadicComplex.valuation_extends`, `PadicComplex.coe_eq`, `PadicComplex.norm_def`, `PadicComplex.coe_natCast`, `instUniformContinuousConstSMulPadic`, `valuation_p`, `PadicComplex.valuation_p`, `PadicComplex.isNonarchimedean`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `valuation_def`, `valuation_coe`, `PadicComplex.coe_zero`, `PadicComplex.norm_extends`, `PadicComplex.rankOne_hom_eq`, `PadicComplex.nnnorm_extends`, `PadicComplexInt.integers`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq` 📖	mathematical	—	`Padic` `PadicAlgCl` `instCoePadic` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Padic.field` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `RingHom.instFunLike` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id`	—	—
`instIsUltrametricDist` 📖	mathematical	—	`IsUltrametricDist` `PadicAlgCl` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `normedField`	—	`IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm` `isNonarchimedean`
`instUniformContinuousConstSMulPadic` 📖	mathematical	—	`UniformContinuousConstSMul` `Padic` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `valued` `AlgebraicClosure.instSMulOfIsScalarTower` `Padic.field` `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` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `Padic` `PadicAlgCl` `Padic.instCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `AlgebraicClosure.instField` `Padic.field` `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` `AlgebraicClosure.isAlgebraic`
`norm_extends` 📖	mathematical	—	`Norm.norm` `PadicAlgCl` `NormedField.toNorm` `normedField` `DFunLike.coe` `RingHom` `Padic` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Padic.field` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `RingHom.instFunLike` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id` `Padic.instNorm`	—	`spectralAlgNorm_extends` `Padic.instIsUltrametricDist` `AlgebraicClosure.isAlgebraic`
`spectralNorm_eq` 📖	mathematical	—	`spectralNorm` `Padic` `Padic.normedField` `PadicAlgCl` `AlgebraicClosure.instField` `Padic.field` `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` `instOneNNReal` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`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
`instAlgebraPadic` 📖	CompOp	—
`instNormedField` 📖	CompOp	4 math math: `norm_def`, `isNonarchimedean`, `norm_extends`, `nnnorm_extends`
`instRankOneNNRealV` 📖	CompOp	2 math math: `norm_def`, `rankOne_hom_eq`
`valued` 📖	CompOp	5 math math: `valuation_extends`, `norm_def`, `valuation_p`, `rankOne_hom_eq`, `PadicComplexInt.integers`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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` `Padic.field` `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` `Padic.field` `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`
`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` `NormedField.toNorm` `instNormedField`	—	`UniformSpace.Completion.induction_on₂` `isClosed_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.comp` `continuous_norm` `continuous_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.Completion.topologicalRing` `Continuous.sup` `TopologicalLattice.toContinuousSup` `HasSolidNorm.toTopologicalLattice` `Continuous.norm` `Continuous.fst` `continuous_id'` `Continuous.snd` `UniformSpace.Completion.coe_add` `Valued.toIsUniformAddGroup` `norm_extends` `PadicAlgCl.isNonarchimedean`
`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` `instNormedField` `UniformSpace.Completion.coe'`	—	`NNReal.eq` `norm_extends`
`norm_def` 📖	mathematical	—	`Norm.norm` `PadicComplex` `NormedField.toNorm` `instNormedField` `Valued.norm` `UniformSpace.Completion.instField` `PadicAlgCl` `AlgebraicClosure.instField` `Padic` `Padic.field` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `Valued.isTopologicalDivisionRing` `Field.toDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `valued` `instRankOneNNRealV`	—	—
`norm_extends` 📖	mathematical	—	`Norm.norm` `UniformSpace.Completion` `PadicAlgCl` `Valued.toUniformSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `PadicAlgCl.normedField` `NNReal` `NNReal.instLinearOrderedCommGroupWithZero` `PadicAlgCl.valued` `NormedField.toNorm` `instNormedField` `UniformSpace.Completion.coe'`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `norm_def` `Valued.norm.eq_1` `coe_nnnorm` `IsTopologicalDivisionRing.toIsTopologicalRing` `valuation_extends`
`rankOne_hom_eq` 📖	mathematical	—	`Valuation.RankOne.hom` `PadicComplex` `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.v` `valued` `instRankOneNNRealV` `PadicAlgCl.instRankOneNNRealV`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup`
`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.extension_extends`
`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` `instOneNNReal` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valued.completable` `map_natCast` `RingHom.instRingHomClass` `coe_eq` `valuation_extends` `PadicAlgCl.valuation_p`

PadicComplexInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integers` 📖	mathematical	—	`Valuation.Integers` `PadicComplex` `NNReal` `UniformSpace.Completion.commRing` `PadicAlgCl` `AlgebraicClosure.instCommRing` `Padic` `Padic.field` `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	22 math math: `PadicComplex.valuation_extends`, `PadicComplex.coe_eq`, `PadicComplex.norm_def`, `PadicComplex.coe_natCast`, `PadicAlgCl.isNonarchimedean`, `PadicAlgCl.norm_extends`, `PadicAlgCl.instUniformContinuousConstSMulPadic`, `PadicAlgCl.valuation_p`, `PadicComplex.valuation_p`, `PadicAlgCl.spectralNorm_eq`, `PadicComplex.isNonarchimedean`, `PadicAlgCl.isAlgebraic`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `PadicAlgCl.valuation_def`, `PadicAlgCl.valuation_coe`, `PadicComplex.coe_zero`, `PadicComplex.norm_extends`, `PadicComplex.rankOne_hom_eq`, `PadicAlgCl.coe_eq`, `PadicAlgCl.instIsUltrametricDist`, `PadicComplex.nnnorm_extends`, `PadicComplexInt.integers`
`PadicComplex` 📖	CompOp	8 math math: `PadicComplex.coe_eq`, `PadicComplex.norm_def`, `PadicComplex.coe_natCast`, `PadicComplex.valuation_p`, `PadicComplex.isNonarchimedean`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `PadicComplex.rankOne_hom_eq`, `PadicComplexInt.integers`
`PadicComplexInt` 📖	CompOp	1 math math: `PadicComplexInt.integers`
`«termℂ_[_]»` 📖	CompOp	—
`«term𝓞_ℂ_[_]»` 📖	CompOp	—

---

← Back to Index