Theorem star_mul_self_add_self_mul_star

Modification history

2026-03-10 04:19
Mathlib/LinearAlgebra/Complex/Module.lean
feat: properties of the real and imaginary parts in a complex star module (#36408) …
Modified star_mul_self_add_self_mul_starView on Github →
2025-04-08 20:01
Mathlib/Data/Complex/Module.lean
feat: generalize Mathlib.Data (#23146) …
Modified star_mul_self_add_self_mul_starView on Github →
2024-02-09 09:06
Mathlib/Data/Complex/Module.lean
feat: add `star_mul_self_add_self_mul_star` (#10365) …
Added star_mul_self_add_self_mul_starView on Github →