Commit 2022-12-18 21:16 f0939b2f

feat: port algebra.group.pi (#1088) mathlib3port tracking sha: b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7

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
Changed a name: update_eq_div_mulSingle => update_eq_div_mul_mulSingle, as it involves a multiplication of two mulSingles. (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.)

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?