feat: port Algebra.Algebra.Operations (#2568)

This had some trouble with leanprover/lean4#2074 and leanprover/lean4#1926.
There are also quite a few places where extra unfolding is needed in initializers for new-style structures.



Co-authored-by: Johan Commelin <johan@commelin.net>

Author: eric-wieser

Mathlib.lean

@@ -4,6 +4,7 @@ import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.Hom
+import Mathlib.Algebra.Algebra.Operations
 import Mathlib.Algebra.Algebra.Pi
 import Mathlib.Algebra.Algebra.Prod
 import Mathlib.Algebra.Algebra.RestrictScalars