no goals
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η✝ : Type u₁'
φ : η✝ → Type ?u.526682
inst✝¹⁸ : Ring K
inst✝¹⁷ : StrongRankCondition K
inst✝¹⁶ : AddCommGroup V✝
inst✝¹⁵ : Module K V✝
inst✝¹⁴ : Module.Free K V✝
inst✝¹³ : AddCommGroup V'
inst✝¹² : Module K V'
inst✝¹¹ : Module.Free K V'
inst✝¹⁰ : AddCommGroup V₁
inst✝⁹ : Module K V₁
inst✝⁸ : Module.Free K V₁
inst✝⁷ : (i : η✝) → AddCommGroup (φ i)
inst✝⁶ : (i : η✝) → Module K (φ i)
inst✝⁵ : ∀ (i : η✝), Module.Free K (φ i)
inst✝⁴ : Fintype η✝
V η : Type u
inst✝³ : Fintype η
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Free K V
⊢ Module.rank K (η → V) = ↑(Fintype.card η) * Module.rank K V
rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]