Structures · Topology
UniformContinuousConstSMul
A multiplicative action such that for all c,
the map fun x ↦ c • x is uniformly continuous.
- Shape
- 2 explicit arguments · adds uniformContinuous_const_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Int
- Nat
- Padic
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- UniformSpace.Completion.toComplL
- ContinuousLinearMap.fromCompletion
- UniformSpace.Completion.toComplₗᵢ
- ContinuousLinearMap.completion
- UniformContinuousConstSMul.uniformContinuous_const_smul
- UniformContinuous.const_smul
- UniformContinuous.mul_const'
- IsUnit.smul_uniformity
- ContinuousLinearMap.completion_apply_coe
- UniformContinuous.div_const'
- UniformSpace.Completion.coe_smul
- UniformSpace.Completion.coe_toComplL
- NumberField.InfinitePlace.Completion.algebraMap_toCompletion
- uniformContinuous_div_const'
- UniformSpace.Completion.algebraMap_def
- UniformContinuous.const_mul'
- uniformContinuous_mul_right'
- Valued.instFaithfulSMulCompletionOfUniformContinuousConstSMul
- smul_uniformity₀
- NumberField.InfinitePlace.Completion.instAlgebra
- UniformSpace.Completion.map_smul_eq_mul_coe
- ContinuousLinearMap.fromCompletion.congr_simp
- UniformContinuousConstSMul.instContinuousConstSMul
- UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul
- UniformSpace.Completion.instModule
- ContinuousLinearMap.coe_fromCompletion
- IsUniformInducing.uniformContinuousConstSMul
- uniformContinuous_mul_left'
- ContinuousLinearMap.toAddMonoidHom_completion
- ContinuousLinearMap.toAddMonoidHom_fromCompletion
- ContinuousLinearMap.fromCompletion_unique
- ContinuousLinearMap.fromCompletion_apply_coe
- ContinuousLinearMap.coe_completion
- smul_uniformity
- UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul
- UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul
- UniformConvergenceCLM.instUniformContinuousConstSMul
- MulOpposite.uniformContinuousConstSMul
- UniformContinuousConstSMul.op
- UniformSpace.Completion.instIsScalarTower
- ContinuousLinearMap.uniformContinuousConstSMul
- UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul
- UniformSpace.Completion.algebra
- UniformFun.uniformContinuousConstSMul
- UniformSpace.Completion.coe_toComplₗᵢ
- UniformFunOn.uniformContinuousConstSMul
Ancestors0
No ancestors.