Stream: maths

Jean Lo (Nov 21 2019 at 20:30):

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 (Nov 21 2019 at 20:31):

well we have that for submodules

Jean Lo (Nov 21 2019 at 20:33):

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?

Last updated: May 14 2021 at 18:28 UTC