Theorem: Set.image_smul_set (Jordan/EquivariantMap.lean)

State before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type u_5
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
s : Set α
⊢ ⇑f₁ '' (m • s) = m • ⇑f₁ '' s
Tactic:
simp
State after:
no goals