Completion

📁 Source: Mathlib/Analysis/Normed/Module/Completion.lean

Statistics

Metric	Count
Definitions instNormedAlgebra, instNormedCommRing, instNormedFieldOfCompletableTopField, instNormedRing, instNormedSpace, toComplL, toComplₗᵢ	7
Theorems coe_toComplL, coe_toComplₗᵢ, norm_toComplL	3
Total	10

UniformSpace.Completion

Definitions

Name	Category	Theorems
instNormedAlgebra 📖	CompOp	—
instNormedCommRing 📖	CompOp	—
instNormedFieldOfCompletableTopField 📖	CompOp	—
instNormedRing 📖	CompOp	—
instNormedSpace 📖	CompOp	1 math math: norm_toComplL
toComplL 📖	CompOp	2 math math: norm_toComplL, coe_toComplL
toComplₗᵢ 📖	CompOp	1 math math: coe_toComplₗᵢ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toComplL 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.Completion uniformSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instModule SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike toComplL coe'	—	SeminormedAddCommGroup.to_isUniformAddGroup
coe_toComplₗᵢ 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup instModule SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup LinearIsometry.instFunLike toComplₗᵢ coe'	—	SeminormedAddCommGroup.to_isUniformAddGroup
norm_toComplL 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.Completion uniformSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule instModule SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toIsBoundedSMul ContinuousLinearMap.hasOpNorm instNormedSpace toComplL Real Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap RingHomIsometric.ids IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul

---

← Back to Index