Commit 2023-04-26 18:21 dc7ac07a

View on Github →

chore(algebra/star/basic): generalize quaternion lemmas (#18802) We already had most of these lemmas specialized to quaternions; this generalizes them to any star ring. We should consider replacing quaternion.conj with star in future.

Estimated changes

Modified src/algebra/quaternion.lean

modified theorem quaternion_algebra.conj_conj_mul

modified theorem quaternion_algebra.conj_mul_conj

Modified src/algebra/star/basic.lean

added theorem commute_star_comm

added theorem commute_star_star

added theorem semiconj_by_star_star_star

added theorem star_inj

added theorem star_mul_star

added theorem star_star_mul