Mathlib v3 is deprecated. Go to Mathlib v4

Theorem star_inj

Modification history

2023-04-26 18:21

src/algebra/star/basic.lean

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

Added star_inj View on Github →