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 v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank 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✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
let B i := chooseBasis 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✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := Dfinsupp.basis fun i => B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank 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✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
let b : Basis _ R (⨁ i, M i) := Dfinsupp.basis fun i => B i
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✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := Dfinsupp.basis fun i => B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']