case intro.mk
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✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ Module.rank R (ι →₀ M) = Cardinal.lift (#ι) * Cardinal.lift (Module.rank R M)
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✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type w
⊢ Module.rank R (ι →₀ M) = Cardinal.lift (#ι) * Cardinal.lift (Module.rank R M)
obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
no goals
case intro.mk
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✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ Module.rank R (ι →₀ M) = Cardinal.lift (#ι) * Cardinal.lift (Module.rank R M)
rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
  Cardinal.sum_const]