feat: completion of a nonarchimedean multiplicative group

[trivial1711]

trafficstars

We prove that the completion of a nonarchimedean multiplicative group is a nonarchimedean multiplicative group.

---

• [x] depends on: #12669
• [ ] depends on: #11837

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12669~~
• leanprover-community/mathlib4#11837 By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary ffd4beb28a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ MonoidHom.completion + MonoidHom.completion_coe + MonoidHom.completion_mul + MonoidHom.completion_one + MonoidHom.continuous_completion + MonoidHom.continuous_extension + MonoidHom.extension + MonoidHom.extension_coe + Multipliable.toComplMulHom_tprod + Multipliable.toCompl_tprod + coe_div + coe_inv_of_field + coe_inv_of_group + continuous_toComplMulHom + denseInducing_toCompl + group + hasProd_iff_hasProd_compl + instCommGroup + instDistribMulAction + instDivCompletionOfGroup + instInvCompletionOfGroup + instMulDistribMulAction + instNegCompletion + instNonarchimedeanGroupCompletion + instSMul + instSubCompletion + instance : ContinuousDiv (Completion α) := ⟨uniformContinuous_completion_div.continuous⟩ + instance : ContinuousInv (Completion α) := ⟨uniformContinuous_completion_inv.continuous⟩ + instance : ContinuousMul (Completion α) := ⟨uniformContinuous_completion_mul.continuous⟩ + instance : DivInvMonoid (Completion α) + instance : Monoid (Completion α) + instance [Mul α] : Mul (Completion α) + instance [One α] : One (Completion α) := ⟨(1 : α)⟩ + instance [Pow X M] : Pow (Completion X) M + isDenseInducing_toComplMulHom + multipliable_iff_cauchySeq_finset_and_tprod_mem + multipliable_iff_multipliable_compl_and_tprod_mem + pow_def + toComplMulHom + uniformGroup - AddMonoidHom.completion - AddMonoidHom.completion_add - AddMonoidHom.completion_coe - AddMonoidHom.completion_zero - AddMonoidHom.continuous_completion - AddMonoidHom.continuous_extension - AddMonoidHom.extension - AddMonoidHom.extension_coe - Summable.toCompl_tsum - UniformSpace.Completion.coe_zero - addGroup - coe_add - coe_neg - coe_sub - hasSum_iff_hasSum_compl - instAddCommGroup - instance : AddMonoid (Completion α) - instance : SMul M (Completion X) - instance : SubNegMonoid (Completion α) - instance [Add α] : Add (Completion α) - instance [Neg α] : Neg (Completion α) - instance [Sub α] : Sub (Completion α) - instance [Zero α] : Zero (Completion α) - instance {G : Type*} [AddGroup G] [UniformSpace G] [UniformAddGroup G] [NonarchimedeanAddGroup G] : - instance {M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] : - mul - one - summable_iff_cauchySeq_finset_and_tsum_mem - summable_iff_summable_compl_and_tsum_mem - uniformAddGroup

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.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
106	1	bare open (scoped) Classical

Current commit ffd4beb28a Reference commit 9b434d1b7f

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).