Support of a function composed with a scalar action

We show that the support of x ↦ f (c⁻¹ • x) is equal to c • support f.

theorem mulSupport_comp_inv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Group α] [MulAction α β] [One γ] (c : α) (f : β → γ) : (Function.mulSupport fun (x : β) => f (c⁻¹ • x)) = c • Function.mulSupport f

theorem support_comp_inv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Group α] [MulAction α β] [Zero γ] (c : α) (f : β → γ) : (Function.support fun (x : β) => f (c⁻¹ • x)) = c • Function.support f

Note: to_additive also automatically translates SMul to VAdd, so we give the additive version manually.

theorem mulSupport_comp_inv_smul₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [GroupWithZero α] [MulAction α β] [One γ] {c : α} (hc : c ≠ 0) (f : β → γ) : (Function.mulSupport fun (x : β) => f (c⁻¹ • x)) = c • Function.mulSupport f

theorem support_comp_inv_smul₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [GroupWithZero α] [MulAction α β] [Zero γ] {c : α} (hc : c ≠ 0) (f : β → γ) : (Function.support fun (x : β) => f (c⁻¹ • x)) = c • Function.support f

Note: to_additive also automatically translates SMul to VAdd, so we give the additive version manually.