Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-19 13:00 b479d3bb

View on Github →

feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion (#4902)

Estimated changes

Modified src/algebra/free_algebra.lean

added theorem free_algebra.star_algebra_map

added def free_algebra.star_hom

added theorem free_algebra.star_ι

Modified src/algebra/free_monoid.lean

added theorem free_monoid.star_of

added theorem free_monoid.star_one

Modified src/algebra/ring_quot.lean

added def ring_quot.star_ring

Modified src/data/quaternion.lean

added theorem quaternion_algebra.star_def