image under smul/add/etc

Stream: maths

[Jean Lo]

A few minutes ago I wrote down the line

/-- The image of a set under scalar multiplication. -/
local notation a ` •'' `:74 S:75 := (λ x, a • x) '' S

I was thinking specifically of inflating sets in vector spaces, but then I mentioned it to @Chris Hughes and he pointed out that it could just be an instance:

instance (α : Type*) (β : Type*) [has_scalar α β] :  has_scalar α (set β) :=
⟨λ a B, (λ x, a • x) '' B⟩

This definition (and similar ones for has_add and friends) makes sense whenever a • b does.

I can't help but suspect there's a reason mathlib doesn't already do this, or that there's something to this effect that I just haven't found. Please advise?

[Kenny Lau]

well we have that for submodules

[Jean Lo]

well we have that for submodules

we do, and that's part of the reason i'm suspicious! why for submodules but not for arbitrary subsets of types that have scalar multiplication?