Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-14 21:31 daf8adf1

View on Github →

feat(algebra/star/basic): add ring_hom.has_involutive_star (#17904) Define an instance has_involutive_star for ring homorphisms into a star_ring.

Estimated changes

added theorem ring_hom.star_apply
added theorem ring_hom.star_def