K✝ : Type u
V✝ : Type v
K V : Type u
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Set V := Basis.ofVectorSpaceIndex K V
⊢ (#V) = (#K) ^ Module.rank K V
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ (#V) = (#K) ^ Module.rank K V
let s := Basis.ofVectorSpaceIndex K V
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Set V := Basis.ofVectorSpaceIndex K V
hs : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ (#V) = (#K) ^ Module.rank K V
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Set V := Basis.ofVectorSpaceIndex K V
⊢ (#V) = (#K) ^ Module.rank K V
let hs := Basis.ofVectorSpace K V
no goals
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Set V := Basis.ofVectorSpaceIndex K V
hs : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ (#V) = (#K) ^ Module.rank K V
calc
  (#V) = (#s →₀ K) := Quotient.sound ⟨hs.repr.toEquiv⟩
  _ = (#s → K) := (Quotient.sound ⟨Finsupp.equivFunOnFinite⟩)
  _ = _ := by rw [← Cardinal.lift_inj.1 hs.mk_eq_rank, Cardinal.power_def]
no goals
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Set V := Basis.ofVectorSpaceIndex K V
hs : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ (#↑s → K) = (#K) ^ Module.rank K V
rw [← Cardinal.lift_inj.1 hs.mk_eq_rank, Cardinal.power_def]