Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-12 15:09 f63b8f12

View on Github →

feat(algebra/star/basic): add some helper lemmas about star (#9651) This adds the new lemmas:

  • star_pow
  • star_nsmul
  • star_gsmul
  • star_prod
  • star_div
  • star_div'
  • star_inv
  • star_inv'
  • star_mul' and generalizes the typeclass assumptions from star_ring to star_add_monoid on:
  • star_neg
  • star_sub
  • star_sum

Estimated changes

added theorem star_div'
added theorem star_div
added theorem star_gsmul
added theorem star_inv'
added theorem star_inv
added theorem star_mul'
modified theorem star_neg
added theorem star_nsmul
added theorem star_pow
added theorem star_prod
modified theorem star_sub
modified theorem star_sum