Commit 2021-10-13 09:37 88863864

View on Github →

feat(star/basic): add a star_monoid (units R) instance (#9681) This also moves all the opposite R instances to be adjacent, and add some missing star_module definitions.

Estimated changes

Modified src/algebra/star/basic.lean

deleted theorem op_star

added theorem opposite.op_star

added theorem opposite.unop_star

added theorem units.coe_star

added theorem units.coe_star_inv

deleted theorem unop_star