Pi.Single misnomer

Stream: mathlib4

[Thomas Murrills]

In Algebra.Data.Pi:

/-- The function supported at `i`, with value `x` there, and `1` elsewhere. -/
@[to_additive Pi.Single "The function supported at `i`, with value `x` there, and `0` elsewhere."]
def mulSingle (i : I) (x : f i) : ∀ (j : I), f j :=
  Function.update 1 i x

shouldn't Pi.Single be Pi.single?

[Thomas Murrills]

(Given Pi.Single.{u, v₁} : {I : Type u} → {f : I → Type v₁} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j)

[Thomas Murrills]

The file I'm porting uses this; if it should indeed be Pi.single (like Pi.mulSingle), can I change it to Pi.single everywhere in this PR, or should changing it be a separate PR (which might complicate things, I guess)?

[Thomas Murrills]

Ok, I think Algebra.Group.Pi is ready for review except for this! If people agree I'll change it everywhere it appears (which so far is just Algebra.Group.Pi and Algebra.Data.Pi).

[Thomas Murrills]

Also, is Algebra.Data.Pi missing #align statements for its @[to_additive] definitions? I can fill those in while I'm at it if desired.

[Thomas Murrills]

It's done apart from this, so I'll just make the changes in the last two commits, and if people would rather separate them we can easily rewrite history :)