StructureFiniteness

📁 Source: FLT/Patching/Utils/StructureFiniteness.lean

Statistics

Metric	Count
Definitions `AlgebraTypeCardLT`, `equivOfAlgebra`, `ofAlgebra`, `ModuleTypeCardLT`, `equivOfModule`, `ofModule`, `TopologicalAlgebraTypeCardLT`, `equivOfAlgebra`, `ofAlgebra`, `TopologicalModuleTypeCardLT`, `equivOfModule`, `ofModule`, `instAddCommGroupFinValFstPSigmaTopologicalSpaceT2SpaceModuleContinuousSMul_fLT`, `instAddCommGroupFinValFstSigmaModule_fLT`, `instAlgebraFinValFstPSigmaRingTopologicalSpaceT2SpaceContinuousSMul_fLT`, `instAlgebraFinValFstSigmaRing_fLT`, `instModuleFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceContinuousSMul_fLT`, `instModuleFinValFstSigmaAddCommGroup_fLT`, `instRingFinValFstPSigmaTopologicalSpaceT2SpaceAlgebraContinuousSMul_fLT`, `instRingFinValFstSigmaAlgebra_fLT`, `instTopologicalSpaceFinValFstPSigmaAddCommGroupT2SpaceModuleContinuousSMul_fLT`, `instTopologicalSpaceFinValFstPSigmaRingT2SpaceAlgebraContinuousSMul_fLT`	22
Theorems `isHomeomorph_equivOfAlgebra`, `instContinuousSMulFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceModule_fLT`, `instContinuousSMulFinValFstPSigmaRingTopologicalSpaceT2SpaceAlgebra_fLT`, `instFiniteAddCommGroup_fLT`, `instFiniteAddGroup_fLT`, `instFiniteAddMonoid_fLT`, `instFiniteAlgebraTypeCardLT`, `instFiniteAlgebra_fLT`, `instFiniteCommGroup_fLT`, `instFiniteGroup_fLT`, `instFiniteModuleTypeCardLT`, `instFiniteModule_fLT`, `instFiniteMonoid_fLT`, `instFinitePSigmaAlgebraContinuousSMulOfT2Space_fLT`, `instFinitePSigmaModuleContinuousSMulOfT2Space_fLT`, `instFiniteRing_fLT`, `instFiniteTopologicalAlgebraTypeCardLT`, `instFiniteTopologicalModuleTypeCardLT`, `instFiniteTopologicalSpace_fLT`, `instT2SpaceFinValFstPSigmaAddCommGroupTopologicalSpaceModuleContinuousSMul_fLT`, `instT2SpaceFinValFstPSigmaRingTopologicalSpaceAlgebraContinuousSMul_fLT`	21
Total	43

AlgebraTypeCardLT

Definitions

Name	Category	Theorems
`equivOfAlgebra` 📖	CompOp	—
`ofAlgebra` 📖	CompOp	—

ModuleTypeCardLT

Definitions

Name	Category	Theorems
`equivOfModule` 📖	CompOp	—
`ofModule` 📖	CompOp	—

TopologicalAlgebraTypeCardLT

Definitions

Name	Category	Theorems
`equivOfAlgebra` 📖	CompOp	1 math math: `isHomeomorph_equivOfAlgebra`
`ofAlgebra` 📖	CompOp	1 math math: `isHomeomorph_equivOfAlgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHomeomorph_equivOfAlgebra` 📖	mathematical	—	`ofAlgebra` `instTopologicalSpaceFinValFstPSigmaRingT2SpaceAlgebraContinuousSMul_fLT` `instRingFinValFstPSigmaTopologicalSpaceT2SpaceAlgebraContinuousSMul_fLT` `instAlgebraFinValFstPSigmaRingTopologicalSpaceT2SpaceContinuousSMul_fLT` `equivOfAlgebra`	—	—

TopologicalModuleTypeCardLT

Definitions

Name	Category	Theorems
`equivOfModule` 📖	CompOp	—
`ofModule` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`AlgebraTypeCardLT` 📖	CompOp	1 math math: `instFiniteAlgebraTypeCardLT`
`ModuleTypeCardLT` 📖	CompOp	1 math math: `instFiniteModuleTypeCardLT`
`TopologicalAlgebraTypeCardLT` 📖	CompOp	1 math math: `instFiniteTopologicalAlgebraTypeCardLT`
`TopologicalModuleTypeCardLT` 📖	CompOp	1 math math: `instFiniteTopologicalModuleTypeCardLT`
`instAddCommGroupFinValFstPSigmaTopologicalSpaceT2SpaceModuleContinuousSMul_fLT` 📖	CompOp	1 math math: `instContinuousSMulFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceModule_fLT`
`instAddCommGroupFinValFstSigmaModule_fLT` 📖	CompOp	—
`instAlgebraFinValFstPSigmaRingTopologicalSpaceT2SpaceContinuousSMul_fLT` 📖	CompOp	2 math math: `TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra`, `instContinuousSMulFinValFstPSigmaRingTopologicalSpaceT2SpaceAlgebra_fLT`
`instAlgebraFinValFstSigmaRing_fLT` 📖	CompOp	—
`instModuleFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceContinuousSMul_fLT` 📖	CompOp	1 math math: `instContinuousSMulFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceModule_fLT`
`instModuleFinValFstSigmaAddCommGroup_fLT` 📖	CompOp	—
`instRingFinValFstPSigmaTopologicalSpaceT2SpaceAlgebraContinuousSMul_fLT` 📖	CompOp	2 math math: `TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra`, `instContinuousSMulFinValFstPSigmaRingTopologicalSpaceT2SpaceAlgebra_fLT`
`instRingFinValFstSigmaAlgebra_fLT` 📖	CompOp	—
`instTopologicalSpaceFinValFstPSigmaAddCommGroupT2SpaceModuleContinuousSMul_fLT` 📖	CompOp	2 math math: `instT2SpaceFinValFstPSigmaAddCommGroupTopologicalSpaceModuleContinuousSMul_fLT`, `instContinuousSMulFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceModule_fLT`
`instTopologicalSpaceFinValFstPSigmaRingT2SpaceAlgebraContinuousSMul_fLT` 📖	CompOp	3 math math: `TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra`, `instContinuousSMulFinValFstPSigmaRingTopologicalSpaceT2SpaceAlgebra_fLT`, `instT2SpaceFinValFstPSigmaRingTopologicalSpaceAlgebraContinuousSMul_fLT`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousSMulFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceModule_fLT` 📖	mathematical	—	`instAddCommGroupFinValFstPSigmaTopologicalSpaceT2SpaceModuleContinuousSMul_fLT` `instModuleFinValFstPSigmaAddCommGroupTopologicalSpaceT2SpaceContinuousSMul_fLT` `instTopologicalSpaceFinValFstPSigmaAddCommGroupT2SpaceModuleContinuousSMul_fLT`	—	—
`instContinuousSMulFinValFstPSigmaRingTopologicalSpaceT2SpaceAlgebra_fLT` 📖	mathematical	—	`instRingFinValFstPSigmaTopologicalSpaceT2SpaceAlgebraContinuousSMul_fLT` `instAlgebraFinValFstPSigmaRingTopologicalSpaceT2SpaceContinuousSMul_fLT` `instTopologicalSpaceFinValFstPSigmaRingT2SpaceAlgebraContinuousSMul_fLT`	—	—
`instFiniteAddCommGroup_fLT` 📖	—	—	—	—	`instFiniteAddGroup_fLT`
`instFiniteAddGroup_fLT` 📖	—	—	—	—	—
`instFiniteAddMonoid_fLT` 📖	—	—	—	—	—
`instFiniteAlgebraTypeCardLT` 📖	mathematical	—	`AlgebraTypeCardLT`	—	`instFiniteRing_fLT` `instFiniteAlgebra_fLT`
`instFiniteAlgebra_fLT` 📖	—	—	—	—	`instFiniteModule_fLT`
`instFiniteCommGroup_fLT` 📖	—	—	—	—	`instFiniteGroup_fLT`
`instFiniteGroup_fLT` 📖	—	—	—	—	—
`instFiniteModuleTypeCardLT` 📖	mathematical	—	`ModuleTypeCardLT`	—	`instFiniteAddCommGroup_fLT` `instFiniteModule_fLT`
`instFiniteModule_fLT` 📖	—	—	—	—	—
`instFiniteMonoid_fLT` 📖	—	—	—	—	—
`instFinitePSigmaAlgebraContinuousSMulOfT2Space_fLT` 📖	—	—	—	—	`instFinitePSigmaModuleContinuousSMulOfT2Space_fLT`
`instFinitePSigmaModuleContinuousSMulOfT2Space_fLT` 📖	—	—	—	—	`Algebra.TopologicallyFG.out` `Algebra.TopologicallyFG.module_ext`
`instFiniteRing_fLT` 📖	—	—	—	—	`instFiniteMonoid_fLT` `instFiniteAddMonoid_fLT`
`instFiniteTopologicalAlgebraTypeCardLT` 📖	mathematical	—	`TopologicalAlgebraTypeCardLT`	—	`instFiniteRing_fLT` `instFiniteTopologicalSpace_fLT` `instFinitePSigmaAlgebraContinuousSMulOfT2Space_fLT`
`instFiniteTopologicalModuleTypeCardLT` 📖	mathematical	—	`TopologicalModuleTypeCardLT`	—	`instFiniteAddCommGroup_fLT` `instFiniteTopologicalSpace_fLT` `instFinitePSigmaModuleContinuousSMulOfT2Space_fLT`
`instFiniteTopologicalSpace_fLT` 📖	—	—	—	—	—
`instT2SpaceFinValFstPSigmaAddCommGroupTopologicalSpaceModuleContinuousSMul_fLT` 📖	mathematical	—	`instTopologicalSpaceFinValFstPSigmaAddCommGroupT2SpaceModuleContinuousSMul_fLT`	—	—
`instT2SpaceFinValFstPSigmaRingTopologicalSpaceAlgebraContinuousSMul_fLT` 📖	mathematical	—	`instTopologicalSpaceFinValFstPSigmaRingT2SpaceAlgebraContinuousSMul_fLT`	—	—

---

← Back to Index