Theorem star_mul_self_eq_realPart_sq_add_imaginaryPart_sq

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) …
Added star_mul_self_eq_realPart_sq_add_imaginaryPart_sqView on Github →