R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) < ℵ₀
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ Module.rank R M < ℵ₀
simp only [Module.rank_def]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) < ℵ₀
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) < ℵ₀
letI := nontrivial_of_invariantBasisNumber R
case intro
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
S : Finset M
hS : Submodule.span R ↑S = ⊤
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) < ℵ₀
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) < ℵ₀
obtain ⟨S, hS⟩ := Module.finite_def.mp ‹Module.Finite R M›
case intro
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
S : Finset M
hS : Submodule.span R ↑S = ⊤
i : { s // LinearIndependent R Subtype.val }
⊢ (#↑↑i) ≤ ↑(Finset.card S)
case intro
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
S : Finset M
hS : Submodule.span R ↑S = ⊤
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) < ℵ₀
refine' (ciSup_le' fun i => _).trans_lt (nat_lt_aleph0 S.card)
no goals
case intro
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
S : Finset M
hS : Submodule.span R ↑S = ⊤
i : { s // LinearIndependent R Subtype.val }
⊢ (#↑↑i) ≤ ↑(Finset.card S)
exact linearIndependent_le_span_finset _ i.prop S hS