mathlib
3ca16d0a - feat(data/equiv): define `ring_equiv_class` (#11977)

Commit
3 years ago
feat(data/equiv): define `ring_equiv_class` (#11977) This PR applies the morphism class pattern to `ring_equiv`, producing a new `ring_equiv_class` extending `mul_equiv_class` and `add_equiv_class`. It also provides a `ring_equiv_class` instance for `alg_equiv`s. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Author
Parents
Loading