Mathlib v3 is deprecated. Go to Mathlib v4

Def ring_quot.star_ring

Modification history

2020-11-19 13:00
src/algebra/ring_quot.lean
feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion (#4902)
Added ring_quot.star_ringView on Github →