Commit 2026-03-10 04:19 98ece81f

feat: properties of the real and imaginary parts in a complex star module (#36408) This expands the API for StarModule ℂ A to include a number of standard results concerning realPart and imaginaryPart. In particular, we provide extensionality lemmas, a characterization of when the real and imaginary parts commute, characterization of unitary elements in terms of real and imaginary parts, as well as a few other fundamental but useful lemmas.