no goals
R : Type u
M✝ : Type v
N✝ : Type w
inst✝¹⁵ : CommRing R
inst✝¹⁴ : StrongRankCondition R
inst✝¹³ : AddCommGroup M✝
inst✝¹² : Module R M✝
inst✝¹¹ : Module.Free R M✝
inst✝¹⁰ : Module.Finite R M✝
inst✝⁹ : AddCommGroup N✝
inst✝⁸ : Module R N✝
inst✝⁷ : Module.Free R N✝
inst✝⁶ : Module.Finite R N✝
M : Type v
N : Type w
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
⊢ finrank R (M ⊗[R] N) = finrank R M * finrank R N
simp [finrank]