Compact

📁 Source: Mathlib/Topology/Algebra/Module/Compact.lean

Statistics

Metric	Count
Definitions	0
Theorems isCompact_of_fg, isClosed_ideal, compactSpace, isCompact_of_fg	4
Total	4

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_of_fg 📖	mathematical	FG CommSemiring.toSemiring	IsCompact SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Submodule.isCompact_of_fg IsTopologicalSemiring.toContinuousAdd ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_ideal 📖	mathematical	—	IsClosed SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsCompact.isClosed Ideal.isCompact_of_fg IsTopologicalRing.toIsTopologicalSemiring IsNoetherian.noetherian

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace	—	Submodule.isCompact_of_fg fg_top

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_of_fg 📖	mathematical	FG CommSemiring.toSemiring	IsCompact SetLike.coe Submodule setLike	—	RingHomSurjective.ids Fintype.range_linearCombination Subtype.range_coe_subtype isCompact_range Function.compactSpace continuous_finset_sum Continuous.smul continuous_apply continuous_const

---

← Back to Index