Theorem Quaternion.star_mul_eq_coe

Modification history

2025-09-24 03:26
Mathlib/Algebra/Quaternion.lean
chore: remove some 'nonrec' (#19907) …
Added Quaternion.star_mul_eq_coeView on Github →