Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 01:36 ae14f6ad

View on Github →

chore(algebra/star): generalize star_bit0, add star_inv_of (#11951)

Estimated changes

modified theorem star_bit0
modified theorem star_bit1
added theorem star_inv_of