Skip to content

Commit

Permalink
feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and simi…
Browse files Browse the repository at this point in the history
…lar 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.
  • Loading branch information
raghuram-13 authored and callesonne committed May 16, 2024
1 parent 3d67461 commit 97cbbf8
Show file tree
Hide file tree
Showing 2 changed files with 535 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -612,6 +612,7 @@ import Mathlib.Algebra.Ring.Defs
import Mathlib.Algebra.Ring.Divisibility.Basic
import Mathlib.Algebra.Ring.Divisibility.Lemmas
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Algebra.Ring.Ext
import Mathlib.Algebra.Ring.Fin
import Mathlib.Algebra.Ring.Hom.Basic
import Mathlib.Algebra.Ring.Hom.Defs
Expand Down
Loading

0 comments on commit 97cbbf8

Please sign in to comment.