mathlib3
ec2dfcae - feat(ring_theory/ring_invo): add ring_invo_class (#18175)

Commit
2 years ago
feat(ring_theory/ring_invo): add ring_invo_class (#18175) By its docstring, `ring_equiv_class` yearns to be extended whenever `ring_equiv` is. The `ring_invo` structure fails to heed its call. This file is currently being ported to mathlib4, and this will help, I believe.
Author
Parents
Loading