## Stream: Beginner Questions

### Topic: locale for vector spaces

#### zibo yang (Apr 21 2021 at 22:42):

Hi, I have a very stupid but weird question. If I get the locale like that:

``````locale real_vector_space = abelian_group V add zero
for V and add (infixl "+" 70) and zero ("๐ฌ") +
fixes scale:: "real โ 'a โ 'a" (infixr "โโฉโ" 75)
assumes scale_add: "โฆx โ V; y โ Vโง โน r โโฉโ (x + y) = r โโฉโ x + r โโฉโ y"
and add_scale: "x โ V โน (r + s) โโฉโ x = r โโฉโ x + s โโฉโ x"
and scale_scale: "x โ V โน r โโฉโ s โโฉโ x = (r * s) โโฉโ x"
and one_scale: "x โ V โน 1 โโฉโ x = x"
``````

then how can I prove

``````x โ V โน r โโฉโ x โ V
``````

since I find it nothing feedback when I code like "using scale_def"

#### Mathias Fleury (Apr 22 2021 at 05:13):

Well, first, `scale` is not defined through a definition. Instead it is an arbitrary constant that has 4 properties (`scale_add`, `add_scale`, `scale_scale`, and `one_scale`). Hence there is no definition (I don't even see what you expect here).

#### Mathias Fleury (Apr 22 2021 at 05:20):

And for you actual question, you need to assume that `โโฉโ` stays in `V`. If you look at the module definition in the Isabelle Library (`~~/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy`), this is what it is done:

``````locale module_on =
fixes S and scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
assumes [...]
and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
``````

#### zibo yang (Apr 22 2021 at 06:05):

Thanks, I got it. let me think a while

#### Anthony Bordg (Apr 22 2021 at 08:51):

@zibo yang As pointed out by Mathias, in `locale real_vector_space` the closure property of `scale` has been forgotten and needs to be added among the assumptions within the locale.

Last updated: Aug 13 2022 at 05:18 UTC