ι : Type u_2
ι' : Type ?u.52430
R : Type u_3
R₂ : Type ?u.52436
K : Type ?u.52439
M : Type u_1
M' : Type ?u.52445
M'' : Type ?u.52448
V : Type u
V' : Type ?u.52453
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
⊢ ↑↑(LinearEquiv.symm b.repr) (↑b.repr x) = x
ι : Type u_2
ι' : Type ?u.52430
R : Type u_3
R₂ : Type ?u.52436
K : Type ?u.52439
M : Type u_1
M' : Type ?u.52445
M'' : Type ?u.52448
V : Type u
V' : Type ?u.52453
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
⊢ ↑(Finsupp.total ι M R ↑b) (↑b.repr x) = x
rw [← b.coe_repr_symm]
no goals
ι : Type u_2
ι' : Type ?u.52430
R : Type u_3
R₂ : Type ?u.52436
K : Type ?u.52439
M : Type u_1
M' : Type ?u.52445
M'' : Type ?u.52448
V : Type u
V' : Type ?u.52453
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
⊢ ↑↑(LinearEquiv.symm b.repr) (↑b.repr x) = x
exact b.repr.symm_apply_apply x