The dimension of a square of a free module

Mathlib's Module.finrank_prod computes the dimension of M × M' for finite free modules. For M × M no finiteness is needed: if M is not finite then neither is M × M, and both dimensions are 0 by convention. So finrank (M × M) = 2 * finrank M for every free module M over a semiring with the strong rank condition (Module.finrank_prod_self).

theorem Module.finrank_prod_self (R : Type u_1) (M : Type u_2) [Semiring R] [StrongRankCondition R] [AddCommMonoid M] [Module R M] [Free R M] : finrank R (M × M) = 2 * finrank R M

The dimension of M × M is twice that of M, whether or not M is finite.