ι : 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
f : Module.End R M
h : ↑(PiToModule.fromMatrix R b) A = ↑(PiToModule.fromEnd R b) f
r : R
⊢ ↑(PiToModule.fromMatrix R b) (r • A) = ↑(PiToModule.fromEnd R b) (r • f)
ι : 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
f : Module.End R M
h : Represents b A f
r : R
⊢ Represents b (r • A) (r • f)
delta Matrix.Represents at h ⊢
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
f : Module.End R M
h : ↑(PiToModule.fromMatrix R b) A = ↑(PiToModule.fromEnd R b) f
r : R
⊢ ↑(PiToModule.fromMatrix R b) (r • A) = ↑(PiToModule.fromEnd R b) (r • f)
rw [SMulHomClass.map_smul, SMulHomClass.map_smul, h]