Theorems · Inductive type · functional analysis
ClosedSubmodule
(R : Type u_2) → (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [TopologicalSpace M] → [Module R M] → Type u_3
The type of closed submodules of a topological module.
- Cited by
- 123 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 5 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- Modulestatement · cited by 20,661
- Semiringstatement · cited by 13,802
- AddCommMonoidstatement · cited by 12,281
Cited by145
Results whose statement or proof uses this declaration.
- ProperConeproof · cited by 57
- ClosedSubmodule.toSubmodulestatement and proof · cited by 51
- ClosedSubmodule.orthogonalstatement and proof · cited by 32
- Submodule.closurestatement · cited by 16
- ClosedSubmodule.mulIstatement and proof · cited by 16
- ClosedSubmodule.extstatement and proof · cited by 15
- ClosedSubmodule.mapEquivstatement and proof · cited by 11
- ClosedSubmodule.comapstatement and proof · cited by 7
- ClosedSubmodule.symplCompstatement and proof · cited by 7
- Submodule.coe_closurestatement · cited by 6
- StandardSubspace.toClosedSubmodulestatement · cited by 6
- ClosedSubmodule.isClosed'statement and proof · cited by 4