Documentation Verification Report

ModuleTopology

📁 Source: FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean

Statistics

Metric	Count
Definitions `equivFun_homeo`, `continuousAlgEquivOfAlgEquiv`, `continuousAlgEquivOfIsScalarTower`, `continuousLinearEquiv`, `leftAlgebra`, `leftModule`, `rightAlgebra`, `rightModule`	8
Theorems `moduleTopology_le`, `equivFun_homeo_apply`, `equivFun_homeo_symm_apply`, `continuous_bilinear_of_finite_free`, `topologicalRing`, `instLeftAlgebra`, `instLeftModule`, `instRightAlgebra`, `instRightModule`, `continuousAlgEquivOsIfScalarTower_apply`, `continuousLinearEquiv_apply`, `continuousLinearEquiv_symm_apply`, `continuous_mul`, `continuous_mul'`, `iff_Continuous_algebraMap`, `instProd'`, `isTopologicalModule`, `locallyCompactSpaceOfFinite`, `of_continuous_isOpenMap_algebraMap`, `of_inverse`, `of_isOpenMap_surjective`, `of_isQuotientMap`, `t2Space`, `t2Space'`, `topologicalSemiring`, `trans`, `secondCountabletopology`, `iff`, `isModuleTopology`, `instFinite_leftAlgebra`, `instFinite_rightAlgebra`, `trans`	32
Total	40

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`moduleTopology_le` 📖	—	—	—	—	`IsTopologicalModule.toContinuousSMul`

IsModuleTopology

Definitions

Name	Category	Theorems
`continuousAlgEquivOfAlgEquiv` 📖	CompOp	—
`continuousAlgEquivOfIsScalarTower` 📖	CompOp	1 math math: `continuousAlgEquivOsIfScalarTower_apply`
`continuousLinearEquiv` 📖	CompOp	2 math math: `continuousLinearEquiv_symm_apply`, `continuousLinearEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAlgEquivOsIfScalarTower_apply` 📖	mathematical	—	`continuousAlgEquivOfIsScalarTower`	—	—
`continuousLinearEquiv_apply` 📖	mathematical	—	`continuousLinearEquiv`	—	—
`continuousLinearEquiv_symm_apply` 📖	mathematical	—	`continuousLinearEquiv`	—	—
`continuous_mul` 📖	—	—	—	—	—
`continuous_mul'` 📖	—	—	—	—	—
`iff_Continuous_algebraMap` 📖	mathematical	—	`IsTopologicalModule`	—	`IsTopologicalModule.toContinuousSMul`
`instProd'` 📖	mathematical	—	`Prod.leftModule` `Prod.rightModule`	—	`Prod.instLeftModule` `Prod.instRightModule`
`isTopologicalModule` 📖	mathematical	—	`IsTopologicalModule`	—	—
`locallyCompactSpaceOfFinite` 📖	—	—	—	—	—
`of_continuous_isOpenMap_algebraMap` 📖	—	—	—	—	`ModuleTopology.isModuleTopology`
`of_inverse` 📖	—	—	—	—	`of_isQuotientMap`
`of_isOpenMap_surjective` 📖	—	—	—	—	`of_isQuotientMap`
`of_isQuotientMap` 📖	—	—	—	—	`ModuleTopology.iff`
`t2Space` 📖	—	—	—	—	—
`t2Space'` 📖	—	—	—	—	`t2Space`
`topologicalSemiring` 📖	—	—	—	—	`continuous_mul'`
`trans` 📖	—	—	—	—	`ModuleTopology.iff` `moduleTopology.trans`

IsModuleTopology.Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_bilinear_of_finite_free` 📖	—	—	—	—	—
`topologicalRing` 📖	—	—	—	—	`IsModuleTopology.continuous_mul`

IsModuleTopology.Module.Basis

Definitions

Name	Category	Theorems
`equivFun_homeo` 📖	CompOp	2 math math: `equivFun_homeo_symm_apply`, `equivFun_homeo_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivFun_homeo_apply` 📖	mathematical	—	`equivFun_homeo`	—	—
`equivFun_homeo_symm_apply` 📖	mathematical	—	`equivFun_homeo`	—	—

IsModuleTopology.Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLeftAlgebra` 📖	mathematical	—	`Prod.leftAlgebra`	—	`IsModuleTopology.of_continuous_isOpenMap_algebraMap`
`instLeftModule` 📖	mathematical	—	`Prod.leftModule`	—	`IsModuleTopology.trans` `Prod.instFinite_leftAlgebra` `instLeftAlgebra`
`instRightAlgebra` 📖	mathematical	—	`Prod.rightAlgebra`	—	`IsModuleTopology.of_continuous_isOpenMap_algebraMap`
`instRightModule` 📖	mathematical	—	`Prod.rightModule`	—	`IsModuleTopology.trans` `Prod.instFinite_rightAlgebra` `instRightAlgebra`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`secondCountabletopology` 📖	—	—	—	—	—

ModuleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff` 📖	—	—	—	—	—
`isModuleTopology` 📖	—	—	—	—	—

Prod

Definitions

Name	Category	Theorems
`leftAlgebra` 📖	CompOp	1 math math: `IsModuleTopology.Prod.instLeftAlgebra`
`leftModule` 📖	CompOp	3 math math: `IsModuleTopology.instProd'`, `IsModuleTopology.Prod.instLeftModule`, `instFinite_leftAlgebra`
`rightAlgebra` 📖	CompOp	1 math math: `IsModuleTopology.Prod.instRightAlgebra`
`rightModule` 📖	CompOp	3 math math: `IsModuleTopology.instProd'`, `IsModuleTopology.Prod.instRightModule`, `instFinite_rightAlgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinite_leftAlgebra` 📖	mathematical	—	`leftModule`	—	—
`instFinite_rightAlgebra` 📖	mathematical	—	`rightModule`	—	—

moduleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans` 📖	—	—	—	—	`IsModuleTopology.isTopologicalModule` `Algebra.moduleTopology_le` `ModuleTopology.isModuleTopology`

---

← Back to Index