Commit 2023-09-08 11:01 c48c769c

feat: flesh out the API for realPart and imaginaryPart (#7023) Improve API for the realPart and imaginaryPart maps in a star module over ℂ.

1. remove the simp attribute on realPart_apply_coe and imaginaryPart_apply_coe
2. construct the ℝ-linear equivalence Complex.selfAdjointEquiv between selfAdjoint ℂ and ℝ. In fact, this would be an algebra equivalence, but that requires selfAdjoint ℂ to have an algebra ℝ (selfAdjoint ℂ) structure, which it doesn't have.
3. show the span (over ℂ) of selfAdjoint A is ⊤ : Submodule ℂ A