ι : Type u_1
ι' : Type ?u.147575
κ : Type ?u.147578
κ' : Type ?u.147581
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.147774
M₂ : Type ?u.147777
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
⊢ (fun i j => ↑(↑e.repr (↑e j)) i) = 1
ι : Type u_1
ι' : Type ?u.147575
κ : Type ?u.147578
κ' : Type ?u.147581
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.147774
M₂ : Type ?u.147777
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
⊢ toMatrix e ↑e = 1
unfold Basis.toMatrix
case a.h
ι : Type u_1
ι' : Type ?u.147575
κ : Type ?u.147578
κ' : Type ?u.147581
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.147774
M₂ : Type ?u.147777
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(↑e.repr (↑e j)) i = OfNat.ofNat 1 i j
ι : Type u_1
ι' : Type ?u.147575
κ : Type ?u.147578
κ' : Type ?u.147581
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.147774
M₂ : Type ?u.147777
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
⊢ (fun i j => ↑(↑e.repr (↑e j)) i) = 1
ext (i j)
no goals
case a.h
ι : Type u_1
ι' : Type ?u.147575
κ : Type ?u.147578
κ' : Type ?u.147581
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.147774
M₂ : Type ?u.147777
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(↑e.repr (↑e j)) i = OfNat.ofNat 1 i j
simp [Basis.equivFun, Matrix.one_apply, Finsupp.single_apply, eq_comm]