K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.418383
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Module.rank R { x // x ∈ span R (range v) } = (#↑(range v))
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.418383
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
⊢ Module.rank R { x // x ∈ span R (range v) } = (#↑(range v))
haveI := nontrivial_of_invariantBasisNumber R
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.418383
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Module.rank R { x // x ∈ span R (range v) } = (#↑(range v))
rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
  Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]