Mathlib v3 is deprecated. Go to Mathlib v4

Theorem star_eq_iff_star_eq

Modification history

2022-02-26 16:53

src/algebra/star/basic.lean

feat(algebra/star/pointwise, algebra/star/basic): add pointwise star, and a few convenience lemmas (#12290) …

Added star_eq_iff_star_eq View on Github →