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 ℂ.