Poll: What should the map `α → Completion α` be called?

Stream: mathlib4

[Mitchell Lee]

Currently, mathlib has several different names for the map from a uniform space to its completion.

• If α is a uniform space with no other structure, it is called (UniformSpace.Completion.coe' : α → Completion α) (though more often written as ((↑) : α → Completion α))
• If α is a uniform additive group, the same function is also a group homomorphism, called (UniformSpace.Completion.toCompl : α →+ Completion α).
• If α is a uniform ring, the same function is also a ring homomorphism, called (UniformSpace.Completion.coeRingHom : α →+* Completion α).
• If α is a normed space over a field 𝕜, the same function is also a linear isometry, called (UniformSpace.Completion.toComplₗᵢ : α →ₗᵢ[𝕜] Completion α).
• If α is a normed space over a field 𝕜, the same function is also a continuous linear map, called (UniformSpace.Completion.toComplL : α →L[𝕜] Completion α).
• If α is a normed additive group, the same function is also a norm-preserving group homomorphism, called (NormedAddCommGroup.toCompl : NormedAddGroupHom α (Completion α))

(As of the merging of #20514 14 hours ago, α is an implicit argument of all six of these functions.)

[Mitchell Lee]

These names are inconsistent. I recently opened #20527, which renames these functions, respectively, to:

• UniformSpace.Completion.coe
• UniformSpace.Completion.coeAddHom
• UniformSpace.Completion.coeRingHom (unchanged)
• UniformSpace.Completion.coeₗᵢ
• UniformSpace.Completion.coeL
• UniformSpace.Completion.coeNormedAddGroupHom

However, @Eric Wieser pointed out (https://github.com/leanprover-community/mathlib4/pull/20527#issuecomment-2574060539) that perhaps these are not the best names either.

[Mitchell Lee]

/poll What should the functions be called?
UniformSpace.Completion.coe, UniformSpace.Completion.coeAddHom, UniformSpace.Completion.coeRingHom, UniformSpace.Completion.coeₗᵢ, UniformSpace.Completion.coeL, UniformSpace.Completion.coeNormedAddGroupHom
UniformSpace.Completion.mk, UniformSpace.Completion.mkAddHom, UniformSpace.Completion.mkRingHom, UniformSpace.Completion.mkₗᵢ, UniformSpace.Completion.mkL, UniformSpace.Completion.mkNormedAddGroupHom
UniformSpace.Completion.of, UniformSpace.Completion.ofAddHom, UniformSpace.Completion.ofRingHom, UniformSpace.Completion.ofₗᵢ, UniformSpace.Completion.ofL, UniformSpace.Completion.ofNormedAddGroupHom