feat: port algebra.group.pi (#1088)

mathlib3port tracking sha: `b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`

### Porting notes

* Moved `AddMonoidWithOne` and `AddGroupWithOne` here from their original files.
* Corrected the name of `Pi.Single` to `Pi.single` in `Data.Pi.Algebra`, on which this depends. (Note: this change was only done in the final two commits, which can be split off into a subsequent PR for a good history if need be.)
* Replaced explicit data fields by sourcing previously-defined instances where possible, as per [this zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/not.20porting.20pi_instance)
* Changed a name: `update_eq_div_mulSingle` => `update_eq_div_mul_mulSingle`, as it involves a multiplication of two `mulSingle`s. (Note: the additive version in mathlib is `update_eq_sub_add_single`, and `to_additive` "agrees" that `update_eq_div_mul_mulSingle` is the right name in mathlib4.)

### Review questions

* Are we sure about using instances as sources where possible? Just want to double-check that it won't cause any problems.
* If so, should the "highest-up" or "lowest-down" instances be used for sourcing when diamonds occur? E.g. `Foo` extends `Bar0`, `Bar1`, and both have relevant instances `bar0`, `bar1`. However, `Bar1` extends `Baz`, and we also have a relevant instance `baz` which suffices for everything not in `Bar0`. Should the instance for `Foo` start `{ bar0, bar1 with ... }` or `{ bar0, baz with ... }`? Does it matter?
* Should the data `mul := (· * ·)`, `zero := (0 : ∀ i, f i)` remain explicit or be obtained by sourcing `Pi.instMul`, `Pi.instZero` respectively?

Author: thorimur

Mathlib.lean

@@ -16,6 +16,7 @@ import Mathlib.Algebra.Group.Ext
 import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.OrderSynonym
+import Mathlib.Algebra.Group.Pi
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Semiconj
 import Mathlib.Algebra.Group.TypeTags