mathlib3

56115334 - feat(analysis/normed_space/star/complex): real and imaginary part of an element of a star module (#11811)

feat(analysis/normed_space/star/complex): real and imaginary part of an element of a star module (#11811) We introduce the real and imaginary parts of an element of a star module, and show that elements of the type can be decomposed into these two parts in the obvious way. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>