no goals
ι : Type ?u.1163482
ι' : Type ?u.1163485
R : Type ?u.1163488
R₂ : Type ?u.1163491
K : Type u_1
M : Type ?u.1163497
M' : Type ?u.1163500
M'' : Type ?u.1163503
V : Type u
V' : Type ?u.1163508
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v : ι → V
s t : Set V
x y z : V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n
classical
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
no goals
ι : Type ?u.1163482
ι' : Type ?u.1163485
R : Type ?u.1163488
R₂ : Type ?u.1163491
K : Type u_1
M : Type ?u.1163497
M' : Type ?u.1163500
M'' : Type ?u.1163503
V : Type u
V' : Type ?u.1163508
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v : ι → V
s t : Set V
x y z : V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩