LinearMapCompletion

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

Statistics

Metric	Count
Definitions completion	1
Theorems coe_completion, completion_apply_coe, toAddMonoidHom_completion	3
Total	4

ContinuousLinearMap

Definitions

Name	Category	Theorems
completion 📖	CompOp	4 math math: completion_apply_coe, toAddMonoidHom_completion, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, coe_completion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_completion 📖	mathematical	—	DFunLike.coe ContinuousLinearMap UniformSpace.Completion UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace AddCommGroup.toAddCommMonoid UniformSpace.Completion.instAddCommGroup UniformSpace.Completion.instModule funLike completion UniformSpace.Completion.map	—	—
completion_apply_coe 📖	mathematical	—	DFunLike.coe ContinuousLinearMap UniformSpace.Completion UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace AddCommGroup.toAddCommMonoid UniformSpace.Completion.instAddCommGroup UniformSpace.Completion.instModule funLike completion UniformSpace.Completion.coe'	—	UniformSpace.Completion.map_coe
toAddMonoidHom_completion 📖	mathematical	—	LinearMap.toAddMonoidHom UniformSpace.Completion AddCommGroup.toAddCommMonoid UniformSpace.Completion.instAddCommGroup UniformSpace.Completion.instModule toLinearMap UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace completion AddMonoidHom.completion AddCommGroup.toAddGroup continuous	—	—

---

← Back to Index