K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.420675
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : LinearIndependent R fun x => ↑x
⊢ Module.rank R { x // x ∈ span R (range Subtype.val) } = (#↑(range Subtype.val))
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.420675
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : LinearIndependent R fun x => ↑x
⊢ Module.rank R { x // x ∈ span R s } = (#↑s)
rw [← @setOf_mem_eq _ s, ← Subtype.range_coe_subtype]
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.420675
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : LinearIndependent R fun x => ↑x
⊢ Module.rank R { x // x ∈ span R (range Subtype.val) } = (#↑(range Subtype.val))
exact rank_span hs