Commit 2024-02-09 09:06 dd92a5cc
View on Github →feat: add star_mul_self_add_self_mul_star
(#10365)
adds the lemma: star a * a + a * star a = 2 • ((ℜ a) ^ 2 + (ℑ a) ^ 2)
for star algebras over ℂ
.
feat: add star_mul_self_add_self_mul_star
(#10365)
adds the lemma: star a * a + a * star a = 2 • ((ℜ a) ^ 2 + (ℑ a) ^ 2)
for star algebras over ℂ
.