Theorem: IsLinearMap.smul_pull (SciLean/Core/Meta/GenerateLinearMapSimp.lean)

State before:
K : Type u'
inst✝⁶ : CommSemiring K
X : Type u
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module K X
Y : Type v
inst✝³ : AddCommGroup Y
inst✝² : Module K Y
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module K Z
f : X → Y
hf : IsLinearMap K f
x : X
k : K
⊢ f (k • x) = k • f x
Tactic:
rw[hf.map_smul]
State after:
no goals