# Zulip Chat Archive

## Stream: maths

### Topic: Unifying `tangent_cone_at` and `pos_tangent_cone_at`

#### Yury G. Kudryashov (Feb 05 2020 at 04:50):

I'd like to prove more properties of tangent cones. With the definitions we have now, I'll have to prove every fact twice: once for `tangent_cone_at`

, and once for `pos_tangent_cone_at`

. I see two ways to unify these definitions:

- Introduce
`(M : submonoid 𝕜)`

in the definition, and require`c n ∈ M`

. This requires coercions here and there. - Define semifields and normed semifields, then
`pos_tangent_cone_at`

becomes`tangent_cone_at nnreal`

.

The second approach looks like the right way to do it but it requires a lot of refactoring. What do you think?

BTW, is there any technical reason to have `module`

and `vector_space`

instead of always dealing with a `semimodule`

?

#### Johan Commelin (Feb 05 2020 at 07:09):

Re `semimodule`

: No, I don't think so. It's just to create a (useful, I think?) air of familiarity for mathematicians

#### Sebastien Gouezel (Feb 05 2020 at 07:41):

I'd like to prove more properties of tangent cones. With the definitions we have now, I'll have to prove every fact twice: once for

`tangent_cone_at`

, and once for`pos_tangent_cone_at`

. I see two ways to unify these definitions:

- Introduce
`(M : submonoid 𝕜)`

in the definition, and require`c n ∈ M`

. This requires coercions here and there.- Define semifields and normed semifields, then
`pos_tangent_cone_at`

becomes`tangent_cone_at nnreal`

.The second approach looks like the right way to do it but it requires a lot of refactoring. What do you think?

I would go for the first way: in any case, there will be coercions involved (in the second approach, you would need to see a real module as an nnreal semimodule), so let's keep it as simple as it can be.

#### Sebastien Gouezel (Feb 05 2020 at 07:45):

BTW, is there any technical reason to have

`module`

and`vector_space`

instead of always dealing with a`semimodule`

?

I have tried to make `module`

and `vector_space`

all abbreviations for `semimodule`

, but some things became too slow. I still think this is a good move, but it will probably have to wait for Lean 4. Link to the conversation: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear.20maps.20over.20semimodule/near/185824677

Last updated: May 09 2021 at 11:09 UTC