Commit 2024-01-23 06:58 5158eea2

feat: case-specific equivalences for IsROrC (#9782) This adds ring isomorphisms and linear isometry equivalences between 𝕜 satisfying IsROrC 𝕜 and ℝ or ℂ depending on whether I = 0 or im I = 1. Of course, the design of IsROrC is meant to eliminate the need for such things most of the time, but these are helpful in the rare case one actually does need to split into the two cases in the middle of a proof.