ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ i : ι, (fun i => A i j * 1) i • b i = ∑ i : ι, A i j • b i
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ↑(↑(fromMatrix R b) A) (Pi.single j 1) = ∑ i : ι, A i j • b i
rw [PiToModule.fromMatrix_apply, Fintype.total_apply, Matrix.mulVec_single]
no goals
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ i : ι, (fun i => A i j * 1) i • b i = ∑ i : ι, A i j • b i
simp_rw [mul_one]