Algebra.Star.SelfAdjoint !4#1860

Stream: mathlib4

[Jireh Loreaux]

I have encountered a number of issues in porting this file:

1. the CommRing and Field instances take way too long (the latter even times out), for no apparent reason.
2. It seems like the issue that @Frédéric Dupuis encountered in this thread is coming up again (see the first two errors in this file). That PR was eventually merged, but neither he nor I knows what the resolution to that problem was, and yet that PR did eventually get merged.
3. Naming: selfAdjoint R : AddSubgroup R, but we frequently (primarily?) use selfAdjoint R as a type in its own right, so SelfAdjoint R seems more appropriate even though selfAdjoint follows the naming conventions. Thoughts?
4. Naming again: when naming a lemma with a Subtype.val coercion, we are supposed to call those val, right? Not coe? It seems Mathlib4 is split on this according to the docs.
5. There were several places where unification in Lean 4 seemed weaker than in Lean 3 (because I had to add type ascriptions). This came up recently in another thread.