Structures · Topology
IsModuleTopology
A class asserting that the topology on a module over a topological ring R is
the module topology. See moduleTopology for more discussion of the module topology.
- Shape
- 2 explicit arguments · adds eq_moduleTopology'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- IsModuleTopology.continuous_of_linearMap
- eq_moduleTopology
- IsModuleTopology.isQuotientMap_of_surjectiveₛₗ
- IsModuleTopology.toContinuousAdd
- IsModuleTopology.isOpenQuotientMap_of_surjectiveₛₗ
- IsModuleTopology.continuous_of_distribMulActionHomₑ
- IsModuleTopology.continuous_bilinear_of_finite_left
- IsModuleTopology.continuous_neg
- IsModuleTopology.continuous_of_linearMapₛₗ
- IsModuleTopology.isoₛₗ
- IsModuleTopology.continuous_of_distribMulActionHom
- IsModuleTopology.isOpenMap_of_surjectiveₛₗ
- IsModuleTopology.isOpenMap_of_surjective
- IsModuleTopology.continuous_bilinear_of_pi_fintype
- IsModuleTopology.eq_moduleTopology'
- IsModuleTopology.iso
- IsModuleTopology.isQuotientMap_of_surjective
- ModuleTopology.eq_coinduced_of_surjectiveₛₗ
- IsModuleTopology.toContinuousSMul
- IsModuleTopology.instPi
- ModuleTopology.eq_coinduced_of_surjective
- IsModuleTopology.instProd
- IsModuleTopology.isTopologicalRing
- IsModuleTopology.topologicalAddGroup
- IsModuleTopology.continuousNeg
- IsModuleTopology.isOpenQuotientMap_of_surjective
- IsModuleTopology.continuous_bilinear_of_finite_right
- IsModuleTopology.continuous_mul_of_finite
- IsModuleTopology.instQuot
- IsModuleTopology.continuous_of_ringHom
Ancestors0
No ancestors.