refactor(Topology/UniformSpace/Completion): more descriptive names for α → Completion α

[trivial1711]

• We rename the various maps α → Completion α in order to make their names more consistent.
  • Let α be a uniform space. We rename the uniformly continuous function α → Completion α from UniformSpace.Completion.coe' to UniformSpace.Completion.coe.
  • Let α be a uniform additive group. We rename the additive group homomorphism α →+ Completion α from UniformSpace.Completion.toCompl to UniformSpace.Completion.coeAddHom.
  • Let α be a uniform ring. The ring homomorphism α →+* Completion α is called UniformSpace.Completion.coeRingHom; its name is unchanged.
  • Let α be a normed space over a field 𝕜. We rename the linear isometry α →ₗᵢ[𝕜] Completion α from UniformSpace.Completion.toComplₗᵢ to UniformSpace.Completion.coeₗᵢ.
  • Let α be a normed space over a field 𝕜. We rename the continuous linear map α →L[𝕜] Completion α from UniformSpace.Completion.toComplL to UniformSpace.Completion.coeL.
  • Let α be a normed additive group. We rename the norm preserving homomorphism NormedAddGroupHom α (Completion α) from NormedAddCommGroup.toCompl to UniformSpace.Completion.coeNormedAddGroupHom.
• We analogously rename some other theorems.
• We add some trivial theorems (all of which are proved by rfl) that state that the functions considered above are equal. We give all of them the simp and norm_cast attributes.
  • We add a new theorem UniformSpace.Completion.coeAddHom_eq_coe that states that UniformSpace.Completion.coeAddHom and UniformSpace.Completion.coe are equal as functions.
  • We similarly add a new theorem UniformSpace.Completion.coeRingHom_eq_coe.
  • We rename the theorem UniformSpace.Completion.coe_toComplₗᵢ to UniformSpace.Completion.coeₗᵢ_eq_coe.
  • We rename the theorem UniformSpace.Completion.coe_toComplL to UniformSpace.Completion.coeL_eq_coe.
  • We similarly add a new theorem UniformSpace.Completion.coeNormedAddGroupHom_eq_coe.
• We change all occurrences of the string ((↑) : α → Completion α) to (coe : α → Completion α) or just coe.
• We put the statements of some theorems into simp normal form by using the plain function coe rather than the homomorphisms that carry more structure.

---

[github-actions]

PR summary c204004f14

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ NormedAddGroupHom.completion_coeNormedAddGroupHom
+ Summable.tsum_coe_completion
+ UniformSpace.Completion.coeNormedAddGroupHom
+ UniformSpace.Completion.coeNormedAddGroupHom_eq_coe
+ UniformSpace.Completion.denseRange_coeNormedAddGroupHom
+ UniformSpace.Completion.hasSum_coe_comp_iff
+ coe
+ coeAddHom
+ coeAddHom_eq_coe
+ coeL
+ coeL_eq_coe
+ coeRingHom_eq_coe
+ coeₗᵢ
+ coeₗᵢ_eq_coe
+ continuous_coeAddHom
+ instance : Coe α (Completion α) := ⟨coe⟩
+ isDenseInducing_coeAddHom
+ norm_coeL
- NormedAddGroupHom.completion_toCompl
- instance : Coe α (Completion α)

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

• We rename the theorem UniformSpace.Completion.coe_toComplₗᵢ to UniformSpace.Completion.coeₗᵢ_eq_coe.
• We rename the theorem UniformSpace.Completion.coe_toComplL to UniformSpace.Completion.coeL_eq_coe.

I think coeFn_coeₗᵢ would be a slightly better name. In the original name, the coe is referring to the ⇑ (DFunLike.coe) on the LHS, not the Completion.coe' on the RHS.

Another way out would be to rename UniformSpace.Completion.coe to UniformSpace.Completion.mk or similar; that way coe is free to remain available for DFunLike.coe.

I agree with the rest of the renaming, but I think it might be worth a zulip poll about coe vs mk vs of vs ...

[trivial1711]

I made the poll: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Poll.3A.20What.20should.20the.20map.20.60.CE.B1.20.E2.86.92.20Completion.20.CE.B1.60.20be.20called.3F/near/492234195

Thanks for the comments.

[eric-wieser]

Thanks, let's leave it a few more days to get more votes