R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring 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
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring 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
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
letI := nontrivial_of_invariantBasisNumber R
no goals
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring 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
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma,
  mk_toNat_eq_card, card_sigma]