∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_3} (R : Type u_4) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] [inst_4 : AddCommMonoid Z] [inst_5 : Module R Z] (f : Y →ₗ[R] Z)
  (m : R) (x : LocallyConstant X Y), LocallyConstant.map (⇑f) (m • x) = (RingHom.id R) m • LocallyConstant.map (⇑f) x