Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 10:15 fb4aee0d

View on Github →

fix(deprecated/*): remove instances (#4735) Remove all instances constructing structures from is_* predicates, like for example:

instance subset.ring {S : set R} [is_subring S] : ring S :=
...

Co-Authored-By: Gabriel Ebner gebner@gebner.org

Estimated changes

added def subtype.group
added def subtype.monoid
added def subring.domain
added def subset.comm_ring
added def subset.ring
added def subtype.ring
added theorem foo
added theorem injective_iff