matrix topology for all dimensions

[zhou31416]

Motivation for this change

PseudoMetricNormedZmodule (and so on) is only defined for matrices of dimension 'M_(m.+1, n.+1) rather than for all dimensions.

Currently, this restriction arises only from the local lemma ball_gt0, so it can be easily removed by redefining mx_ball as follows:
Definition mx_ball x e y := 0 < e /\ forall i j, ball (x i j) e (y i j).

Checklist

No additional lemmas or definitions added.
A minor modification of matrix_topology.v and matrix_normedtype.v
Generalize lemma rV_compact since it holds for all dimensions (rather than non-degenerative cases, i.e., 'M_(m.+1,n.+1).

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[proux01]

FTR, this was discussed in #math-comp analysis > Matrix PseudoMetricNormedZmodule for all dimensions

[CohenCyril]

Thank you for your contribution. This is indeed a very welcome change!

Please fix the proof script: I submitted a (blind) fix, assuming you opened a new line with indentation for a subgoal, which must always be closed with a by / exact / other terminator as per mathcomp conventions. Please test my fix and ping me back.

[CohenCyril]

Suggested change

	rewrite (_ : mkset _ = [set v0]).
	apply: compact_set1.
	rewrite (_ : mkset _ = [set v0]); first exact: compact_set1.

[zhou31416]

Thanks for the suggestion; I’ve fixed it.
I also generalised mx_normZ to work with numDomainType rather than numFieldType.