FiniteDimensional

📁 Source: Mathlib/Topology/Algebra/SeparationQuotient/FiniteDimensional.lean

Statistics

Metric	Count
Definitions FiniteDimensional	1
Theorems instModuleFinite	1
Total	2

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instModuleFinite 📖	mathematical	—	Module.Finite SeparationQuotient instAddCommMonoid instModule	—	Module.Finite.of_surjective RingHomSurjective.ids Quotient.mk_surjective

Topology.RelCWComplex

Definitions

Name	Category	Theorems
FiniteDimensional 📖	CompData	2 math math: Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional, Finite.toFiniteDimensional

---

← Back to Index