!3#18289 invariant submodules

Stream: PR reviews

[Scott Morrison]

A superficial look at @Monica Omar's mathilb3 PR !3#18289 suggests that is has been through some extensive review, but no final decision was ever made. (As on the other thread, apologies to @Monica Omar for this. Porting held a lot of things up.)

Is this PR ready to go?

@Monica Omar, if it is merged as is or after a little more review, would you be able to help forward port it to Mathlib4?

[Monica Omar]

Yeah, I can help with porting it to Mathlib4 after merging!

[Eric Wieser]

I'll do a final round of fixups to this tonight