UniformMulAction

📁 Source: Mathlib/Topology/Algebra/UniformMulAction.lean

Statistics

Metric	Count
Definitions UniformContinuousConstSMul, UniformContinuousConstVAdd, instAddActionOfUniformContinuousConstVAdd, instMulActionOfUniformContinuousConstSMul, instSMul, instVAdd	6
Theorems uniformContinuousConstSMul_int, uniformContinuousConstSMul_nat, uniformContinuousConstVAdd, vadd_uniformity, to_uniformContinuousConstVAdd, to_uniformContinuousConstSMul, uniformContinuousConstSMul, uniformContinuousConstVAdd, smul_uniformity, uniformContinuousConstSMul, uniformContinuousConstSMul, uniformContinuousConstSMul_op, const_mul', const_smul, const_vadd, div_const', mul_const', op, to_continuousConstSMul, uniformContinuous_const_smul, op, to_continuousConstVAdd, uniformContinuous_const_vadd, coe_smul, coe_vadd, instIsCentralScalar, instIsCentralVAdd, instIsScalarTower, instSMulCommClassOfUniformContinuousConstSMul, instUniformContinuousConstSMul, instUniformContinuousConstVAdd, instVAddAssocClass, instVAddCommClassOfUniformContinuousConstVAdd, smul_def, vadd_def, smul_uniformity, smul_uniformity₀, uniformContinuousConstSMul_of_continuousConstSMul, uniformContinuous_div_const', uniformContinuous_mul_left', uniformContinuous_mul_right', vadd_uniformity	42
Total	48

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousConstSMul_int 📖	mathematical	—	UniformContinuousConstSMul SubNegMonoid.toZSMul toSubNegMonoid	—	uniformContinuous_const_zsmul

AddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousConstSMul_nat 📖	mathematical	—	UniformContinuousConstSMul toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	uniformContinuous_const_nsmul

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousConstVAdd 📖	mathematical	—	UniformContinuousConstVAdd AddOpposite instUniformSpaceAddOpposite instVAdd	—	UniformContinuous.comp uniformContinuous_op UniformContinuous.const_vadd uniformContinuous_unop

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
vadd_uniformity 📖	mathematical	IsAddUnit	HVAdd.hVAdd Filter instHVAdd Filter.instVAddFilter Prod.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction uniformity	—	exists_neg UniformContinuousConstVAdd.uniformContinuous_const_vadd le_antisymm vadd_vadd zero_vadd Filter.vadd_filter_le_vadd_filter

IsUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_uniformContinuousConstVAdd 📖	mathematical	—	UniformContinuousConstVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	UniformContinuous.add uniformContinuous_const uniformContinuous_id

IsUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_uniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	UniformContinuous.mul uniformContinuous_const uniformContinuous_id

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousConstSMul 📖	mathematical	IsUniformInducing	UniformContinuousConstSMul	—	uniformContinuous_iff UniformContinuous.const_smul uniformContinuous
uniformContinuousConstVAdd 📖	mathematical	IsUniformInducing HVAdd.hVAdd instHVAdd	UniformContinuousConstVAdd	—	uniformContinuous_iff UniformContinuous.const_vadd uniformContinuous

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_uniformity 📖	mathematical	IsUnit	Filter Filter.instSMulFilter Prod.instSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction uniformity	—	exists_right_inv UniformContinuousConstSMul.uniformContinuous_const_smul le_antisymm smul_smul one_smul Filter.smul_filter_le_smul_filter

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul MulOpposite instUniformSpaceMulOpposite instSMul	—	UniformContinuous.comp uniformContinuous_op UniformContinuous.const_smul uniformContinuous_unop

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne toAddGroupWithOne DistribSMul.toSMulZeroClass instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing toNonAssocRing	—	uniformContinuousConstSMul_of_continuousConstSMul IsScalarTower.continuousConstSMul IsScalarTower.left
uniformContinuousConstSMul_op 📖	mathematical	—	UniformContinuousConstSMul MulOpposite SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero toSemiring Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing toNonAssocRing Semiring.toOppositeModule	—	uniformContinuousConstSMul_of_continuousConstSMul SMulCommClass.continuousConstSMul Semigroup.opposite_smulCommClass

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_mul' 📖	mathematical	UniformContinuous	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	const_smul
const_smul 📖	mathematical	UniformContinuous	Function.hasSMul	—	comp UniformContinuousConstSMul.uniformContinuous_const_smul
const_vadd 📖	mathematical	UniformContinuous	HVAdd.hVAdd instHVAdd Function.hasVAdd	—	comp UniformContinuousConstVAdd.uniformContinuous_const_vadd
div_const' 📖	mathematical	UniformContinuous	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	div_eq_mul_inv mul_const'
mul_const' 📖	mathematical	UniformContinuous	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	const_smul

UniformContinuousConstSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	—	UniformContinuousConstSMul MulOpposite	—	IsCentralScalar.op_smul_eq_smul uniformContinuous_const_smul
to_continuousConstSMul 📖	mathematical	—	ContinuousConstSMul UniformSpace.toTopologicalSpace	—	UniformContinuous.continuous uniformContinuous_const_smul
uniformContinuous_const_smul 📖	mathematical	—	UniformContinuous	—	—

UniformContinuousConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	—	UniformContinuousConstVAdd AddOpposite	—	IsCentralVAdd.op_vadd_eq_vadd uniformContinuous_const_vadd
to_continuousConstVAdd 📖	mathematical	—	ContinuousConstVAdd UniformSpace.toTopologicalSpace	—	UniformContinuous.continuous uniformContinuous_const_vadd
uniformContinuous_const_vadd 📖	mathematical	—	UniformContinuous HVAdd.hVAdd instHVAdd	—	—

UniformSpace.Completion

Definitions

Name	Category	Theorems
instAddActionOfUniformContinuousConstVAdd 📖	CompOp	—
instMulActionOfUniformContinuousConstSMul 📖	CompOp	—
instSMul 📖	CompOp	12 math math: smul_def, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', instSMulCommClassOfUniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, instUniformContinuousConstSMul, PadicComplex.instIsScalarTowerPadicPadicAlgCl, coe_smul, Valued.instFaithfulSMulCompletionOfUniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, instIsCentralScalar, instIsBoundedSMul, instIsScalarTower
instVAdd 📖	CompOp	6 math math: vadd_def, coe_vadd, instUniformContinuousConstVAdd, instVAddAssocClass, instIsCentralVAdd, instVAddCommClassOfUniformContinuousConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	coe' UniformSpace.Completion instSMul	—	map_coe UniformContinuousConstSMul.uniformContinuous_const_smul
coe_vadd 📖	mathematical	—	coe' HVAdd.hVAdd instHVAdd UniformSpace.Completion instVAdd	—	map_coe UniformContinuousConstVAdd.uniformContinuous_const_vadd
instIsCentralScalar 📖	mathematical	—	IsCentralScalar UniformSpace.Completion instSMul MulOpposite	—	IsCentralScalar.op_smul_eq_smul
instIsCentralVAdd 📖	mathematical	—	IsCentralVAdd UniformSpace.Completion instVAdd AddOpposite	—	IsCentralVAdd.op_vadd_eq_vadd
instIsScalarTower 📖	mathematical	—	IsScalarTower UniformSpace.Completion instSMul	—	map_comp UniformContinuousConstSMul.uniformContinuous_const_smul smul_assoc
instSMulCommClassOfUniformContinuousConstSMul 📖	mathematical	—	SMulCommClass UniformSpace.Completion instSMul	—	map_comp UniformContinuousConstSMul.uniformContinuous_const_smul SMulCommClass.smul_comm
instUniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul UniformSpace.Completion uniformSpace instSMul	—	uniformContinuous_map
instUniformContinuousConstVAdd 📖	mathematical	—	UniformContinuousConstVAdd UniformSpace.Completion uniformSpace instVAdd	—	uniformContinuous_map
instVAddAssocClass 📖	mathematical	—	VAddAssocClass UniformSpace.Completion instVAdd	—	map_comp UniformContinuousConstVAdd.uniformContinuous_const_vadd vadd_assoc
instVAddCommClassOfUniformContinuousConstVAdd 📖	mathematical	—	VAddCommClass UniformSpace.Completion instVAdd	—	map_comp UniformContinuousConstVAdd.uniformContinuous_const_vadd VAddCommClass.vadd_comm
smul_def 📖	mathematical	—	UniformSpace.Completion instSMul map	—	—
vadd_def 📖	mathematical	—	HVAdd.hVAdd UniformSpace.Completion instHVAdd instVAdd map	—	—

(root)

Definitions

Name	Category	Theorems
UniformContinuousConstSMul 📖	CompData	20 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', AddMonoid.uniformContinuousConstSMul_nat, MulOpposite.uniformContinuousConstSMul, IsBoundedSMul.toUniformContinuousConstSMul, Ring.uniformContinuousConstSMul, UniformSpace.Completion.instUniformContinuousConstSMul, ContinuousLinearMap.uniformContinuousConstSMul, ContinuousAlternatingMap.instUniformContinuousConstSMul, uniformContinuousConstSMul_of_continuousConstSMul, PadicAlgCl.instUniformContinuousConstSMulPadic, IsUniformInducing.uniformContinuousConstSMul, UniformFunOn.uniformContinuousConstSMul, AddGroup.uniformContinuousConstSMul_int, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, ContinuousMultilinearMap.instUniformContinuousConstSMul, UniformContinuousConstSMul.op, UniformConvergenceCLM.instUniformContinuousConstSMul, UniformFun.uniformContinuousConstSMul, Ring.uniformContinuousConstSMul_op, IsUniformGroup.to_uniformContinuousConstSMul
UniformContinuousConstVAdd 📖	CompData	5 math math: UniformContinuousConstVAdd.op, IsUniformAddGroup.to_uniformContinuousConstVAdd, UniformSpace.Completion.instUniformContinuousConstVAdd, IsUniformInducing.uniformContinuousConstVAdd, AddOpposite.uniformContinuousConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_uniformity 📖	mathematical	—	Filter Filter.instSMulFilter Prod.instSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction uniformity	—	IsUnit.smul_uniformity Group.isUnit
smul_uniformity₀ 📖	mathematical	—	Filter Filter.instSMulFilter Prod.instSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction uniformity	—	IsUnit.smul_uniformity Ne.isUnit
uniformContinuousConstSMul_of_continuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass	—	uniformContinuous_of_continuousAt_zero AddMonoidHom.instAddMonoidHomClass Continuous.continuousAt ContinuousConstSMul.continuous_const_smul
uniformContinuous_div_const' 📖	mathematical	—	UniformContinuous DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	UniformContinuous.div_const' uniformContinuous_id
uniformContinuous_mul_left' 📖	mathematical	—	UniformContinuous Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	UniformContinuous.const_mul' uniformContinuous_id
uniformContinuous_mul_right' 📖	mathematical	—	UniformContinuous Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	UniformContinuous.mul_const' uniformContinuous_id
vadd_uniformity 📖	mathematical	—	HVAdd.hVAdd Filter instHVAdd Filter.instVAddFilter Prod.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction uniformity	—	IsAddUnit.vadd_uniformity AddGroup.isAddUnit

---

← Back to Index