Documentation Verification Report

Infinite

📁 Source: FLT/NumberField/Completion/Infinite.lean

Statistics

Metric	Count
Definitions `baseChange`, `baseChangeEquiv`, `baseChangeEquivRight`, `baseChangeRight`, `comapHom`, `instNontriviallyNormedField_fLT`, `instNormedSpaceValEqComapAlgebraMap_fLT`, `instTopologicalSpaceTensorProduct_fLT`, `piEquiv`, `piExtension`	10
Theorems `baseChangeEquiv_tmul`, `baseChange_injective`, `baseChange_surjective`, `comapHom_cont`, `finrank_pi_eq_finrank_tensorProduct`, `finrank_prod_eq_finrank`, `instFiniteDimensionalValEqComapAlgebraMap_fLT`, `instFreeValEqComapAlgebraMap_fLT`, `instIsModuleTopologyTensorProduct_fLT`, `instIsModuleTopologyValEqComapAlgebraMap_fLT`, `piEquiv_smul`, `piExtension_apply`	12
Total	22

NumberField.InfinitePlace.Completion

Definitions

Name	Category	Theorems
`baseChange` 📖	CompOp	2 math math: `baseChange_surjective`, `baseChange_injective`
`baseChangeEquiv` 📖	CompOp	1 math math: `baseChangeEquiv_tmul`
`baseChangeEquivRight` 📖	CompOp	—
`baseChangeRight` 📖	CompOp	—
`comapHom` 📖	CompOp	4 math math: `piEquiv_smul`, `baseChangeEquiv_tmul`, `comapHom_cont`, `piExtension_apply`
`instNontriviallyNormedField_fLT` 📖	CompOp	—
`instNormedSpaceValEqComapAlgebraMap_fLT` 📖	CompOp	6 math math: `NumberField.InfiniteAdeleRing.instFiberwiseSMulInfinitePlaceCompletion`, `piEquiv_smul`, `instFreeValEqComapAlgebraMap_fLT`, `instFiniteDimensionalValEqComapAlgebraMap_fLT`, `finrank_prod_eq_finrank`, `finrank_pi_eq_finrank_tensorProduct`
`instTopologicalSpaceTensorProduct_fLT` 📖	CompOp	2 math math: `baseChangeEquiv_tmul`, `instIsModuleTopologyTensorProduct_fLT`
`piEquiv` 📖	CompOp	1 math math: `piEquiv_smul`
`piExtension` 📖	CompOp	1 math math: `piExtension_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChangeEquiv_tmul` 📖	mathematical	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `instTopologicalSpaceTensorProduct_fLT` `NumberField.InfinitePlace.Extension` `baseChangeEquiv` `SemialgHom` `WithAbs.instAlgebraReal_fLT` `instFunLike` `comapHom`	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `SemialgHom.baseChange_of_algebraMap_tmul`
`baseChange_injective` 📖	mathematical	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `NumberField.InfinitePlace.Extension` `baseChange`	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `WithAbs.instIsScalarTowerReal_fLT` `SemialgHom.baseChangeRightOfAlgebraMap_coe` `TensorProduct.RightActions.instFinite_fLT` `instFiniteDimensionalValEqComapAlgebraMap_fLT` `finrank_pi_eq_finrank_tensorProduct` `baseChange_surjective`
`baseChange_surjective` 📖	mathematical	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `NumberField.InfinitePlace.Extension` `baseChange`	—	`instFreeValEqComapAlgebraMap_fLT` `instFiniteDimensionalValEqComapAlgebraMap_fLT` `denseRange_algebraMap_subtype_pi` `WithAbs.instUniformContinuousConstSMulReal_fLT` `DenseRange.exists_matrix_det_ne_zero` `Basis.toMatrix_continuous` `WithAbs.instIsScalarTowerReal_fLT` `SemialgHom.baseChangeRightOfAlgebraMap_coe` `SemialgHom.baseChangeRightOfAlgebraMap_apply` `SemialgHom.baseChange_of_algebraMap_tmul_left`
`comapHom_cont` 📖	mathematical	—	`SemialgHom` `WithAbs.instAlgebraReal_fLT` `instFunLike` `comapHom`	—	—
`finrank_pi_eq_finrank_tensorProduct` 📖	mathematical	—	`NumberField.InfinitePlace.Extension` `instNormedSpaceValEqComapAlgebraMap_fLT` `WithAbs.instUniformContinuousConstSMulReal_fLT` `TensorProduct.RightActions.instModule_fLT`	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `finrank_prod_eq_finrank`
`finrank_prod_eq_finrank` 📖	mathematical	—	`NumberField.InfinitePlace.Extension` `instNormedSpaceValEqComapAlgebraMap_fLT`	—	`instFreeValEqComapAlgebraMap_fLT` `instFiniteDimensionalValEqComapAlgebraMap_fLT` `NumberField.InfinitePlace.Extension.sum_ramificationIdx_eq` `finrank_eq_ramificationIdx`
`instFiniteDimensionalValEqComapAlgebraMap_fLT` 📖	mathematical	—	`instNormedSpaceValEqComapAlgebraMap_fLT`	—	—
`instFreeValEqComapAlgebraMap_fLT` 📖	mathematical	—	`instNormedSpaceValEqComapAlgebraMap_fLT`	—	`instFiniteDimensionalValEqComapAlgebraMap_fLT`
`instIsModuleTopologyTensorProduct_fLT` 📖	mathematical	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `TensorProduct.RightActions.instSMul_fLT` `instTopologicalSpaceTensorProduct_fLT`	—	`WithAbs.instUniformContinuousConstSMulReal_fLT`
`instIsModuleTopologyValEqComapAlgebraMap_fLT` 📖	mathematical	—	`instAlgebraValEqComapAlgebraMap_fLT`	—	`instFiniteDimensionalValEqComapAlgebraMap_fLT`
`piEquiv_smul` 📖	mathematical	—	`NumberField.InfinitePlace.Extension` `instNormedSpaceValEqComapAlgebraMap_fLT` `piEquiv` `SemialgHom` `WithAbs.instAlgebraReal_fLT` `instFunLike` `comapHom`	—	—
`piExtension_apply` 📖	mathematical	—	`SemialgHom` `NumberField.InfinitePlace.Extension` `instFunLike` `piExtension` `WithAbs.instAlgebraReal_fLT` `comapHom`	—	—

---

← Back to Index