Pointwise actions of linear maps

theorem image_smul_setₛₗ {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Semiring R] [Semiring S] (σ : R →+* S) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] {F : Type u_7} (h : F) [FunLike F M N] [SemilinearMapClass F σ M N] (c : R) (s : Set M) : ⇑h '' (c • s) = σ c • ⇑h '' s

theorem preimage_smul_setₛₗ {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Semiring R] [Semiring S] (σ : R →+* S) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] {F : Type u_7} (h : F) [FunLike F M N] [SemilinearMapClass F σ M N] {c : R} (hc : IsUnit c) (s : Set N) : ⇑h ⁻¹' (σ c • s) = c • ⇑h ⁻¹' s

@[simp]

theorem image_smul_set (R : Type u_1) (M₁ : Type u_4) (M₂ : Type u_5) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {F : Type u_7} (h : F) [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] (c : R) (s : Set M₁) : ⇑h '' (c • s) = c • ⇑h '' s

theorem preimage_smul_set (R : Type u_1) (M₁ : Type u_4) (M₂ : Type u_5) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {F : Type u_7} (h : F) [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] {c : R} (hc : IsUnit c) (s : Set M₂) : ⇑h ⁻¹' (c • s) = c • ⇑h ⁻¹' s