mathlib3
233433b0 - conj_to_ring_equiv -> abbreviation for star_ring_equiv

Commit

4 years ago

conj_to_ring_equiv -> abbreviation for star_ring_equiv

References

#9692 - refactor(algebra/star): replace `star_ring_aut` with `star`

Author

dupuisf

dupuisf

Parents

Loading