Commit 2024-05-09 04:14 47d4fa91

feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses (#9511) Add a 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.