Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_hom_inv_pair.of_ring_equiv

Modification history

2021-10-14 21:12
src/algebra/ring/comp_typeclasses.lean
feat(algebra/star): star_linear_equiv (#9426)
Added ring_hom_inv_pair.of_ring_equivView on Github →