Mathlib v3 is deprecated. Go to Mathlib v4

Theorem commute_star_star

Modification history

2023-04-26 18:21

src/algebra/star/basic.lean

chore(algebra/star/basic): generalize quaternion lemmas (#18802) …

Added commute_star_star View on Github →