Prove extensionality lemmas for `Ring` and similar typeclasses

[raghuram-13]

trafficstars

feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses

Add file Algebra/Ring/Ext, proving ext lemmas for all of the ring-like classes (for example, anything from NonUnitalNonAssocSemiring to CommRing), stating that two instances of such a class are equal if they define the same addition and multiplication operations. Also prove ext_iff variants for each class, and injectivity lemmas for projections from classes to parent classes.

---

Some notes:

• Things I didn't do because they don't seem particularly necessary:

  • I skipped HasDistribNeg.
  • More injectivity lemmas could be proved between the Comm variants (currently it's just from Comm variant to non-Comm variant for each).

• A natural next step would be to extend this to DivisionSemiring, DivisionRing, Semifield and Field.

• I have introduced local notation to eliminate some boilerplate. I'm not sure if this is style-appropriate for Mathlib (although the notation is local to one file and (probably) never shows up when e.g. the types of lemmas are viewed, so that it's invisible to anyone not editing this file).

• In another branch, I have used a (local) custom command to generate the ext and ext_iff lemmas, eliminating even more boilerplate.

  It should be possible to extend that command to be more general (such as allowing declModifiers and terminationSuffix clauses, allowing a custom theorem name defaulting to ext, specifying the type for which an ext lemma is being proved, specifying the arguments, and letting the names be inaccessible by default while allowing them to be specified with a "with" clause), in which case it could become a useful command for writing extensionality lemmas (admittedly partially overlapping in functionality with putting an @[ext] on the type definition).

• I haven't written any tests — I'm not sure what to test or how to write tests.