feat: IsROrC Rank Lemmas without PartialOrder and StarOrderedRing

[MohanadAhmed]

This PR proves three lemmas rank_conjTranspose_R_or_C, rank_self_mul_conjTranspose_R_or_C and rank_conjTranspose_mul_self_R_or_C which state that in $\mathbb{R}$ or $\mathbb{C}$ fields:

• $\text{rank}(A^H) = \text{rank}(A)$
• $\text{rank}(A^HA) = \text{rank}(A)$
• $\text{rank}(AA^H) = \text{rank}(A)$

These are almost the same named lemmas (without R_or_C suffix). However the original lemmas don't apply without using a PartialOrder and StarOrderedRing on the Complex Field and IsROrC, which seems to be a point the community is still discussing. The lemmas in this PR apply directly WITHOUT requiring PartialOrder and StarOrderedRing.

Co-authored-by: Mohanad Ahmed m.a.m.elhassan@gmail.com

---

[semorrison]

Please change the PR title, this should start with feat:.

[j-loreaux]

I don't think these results are necessary. #6391 will be merged soon, and then these results will be available behind the ComplexOrder scope.

[j-loreaux]

This is too heavy an import for this file. If you need it, it means the results don't belong here.

[j-loreaux]

again, too heavy an import

[j-loreaux]

I don't think this is necessary since it is just map_sum IsROrC.reLm _.

[MohanadAhmed]

I don't think these results are necessary. #6391 will be merged soon, and then these results will be available behind the ComplexOrder scope.

I see.
I think I understand the first point about results will be available through scoped starOrderedRing. But I did not understand the second point about too heavy import? How do you decide if an import is too heavy or not?

Anyway I think I will close this PR for now.

[j-loreaux]

Whether or not an import is "too heavy" or not is a bit subjective. However, the basic question is: are you importing (even transitively) a lot more than was imported previously? If so, is it essential to the file, or only a few declarations? If the latter, then probably it's too heavy. If it is essential for a lot of new material you are adding, maybe it deserves its own new file.