## 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