no goals
ι : Type u_1
ι' : Type ?u.640840
R : Type u_2
R₂ : Type ?u.640846
K : Type ?u.640849
M : Type u_3
M' : Type ?u.640855
M'' : Type ?u.640858
V : Type u
V' : Type ?u.640863
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : Fintype ι
b✝ b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι
classical
  calc
    card M = card (ι → R) := card_congr b.equivFun.toEquiv
    _ = card R ^ card ι := card_fun
no goals
ι : Type u_1
ι' : Type ?u.640840
R : Type u_2
R₂ : Type ?u.640846
K : Type ?u.640849
M : Type u_3
M' : Type ?u.640855
M'' : Type ?u.640858
V : Type u
V' : Type ?u.640863
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : Fintype ι
b✝ b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι
calc
  card M = card (ι → R) := card_congr b.equivFun.toEquiv
  _ = card R ^ card ι := card_fun