Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_star_of_eq_star

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 eq_star_of_eq_star View on Github →