## Stream: PR reviews

### Topic: 3728: define ordered semimodules and generalize convexity...

#### Yury G. Kudryashov (Aug 20 2020 at 03:06):

@Frédéric Dupuis I'm rewriting convexity for affine spaces, and I have a question about your old PR #3728
Many lemmas assume  {β : Type*} [ordered_add_comm_monoid β] [ordered_semimodule ℝ β]. Is there any reason to prefer these assumptions to {γ : Type*} [ordered_cancel_add_comm_monoid γ] [ordered_semimodule ℝ γ]? A (semi)module over ℝ can't be just an add_comm_monoid anyway (unless someone forgot to define an instance).

#### Yury G. Kudryashov (Aug 20 2020 at 03:07):

It makes sense if you're going to generalize to {β : Type*} [ordered_add_comm_monoid β] [ordered_semimodule nnreal β].

#### Yury G. Kudryashov (Aug 20 2020 at 03:08):

Do you need this generalization in some case?

#### Johan Commelin (Aug 20 2020 at 03:08):

@Reid Barton and I were just talking about ordered semimodules yesterday :rofl:

#### Johan Commelin (Aug 20 2020 at 03:08):

Didn't realise there was a PR :see_no_evil:

#### Johan Commelin (Aug 20 2020 at 03:09):

/me should learn what is in mathlib!

#### Johan Commelin (Aug 20 2020 at 03:09):

That's what you get for going on holidays

#### Johan Commelin (Aug 20 2020 at 03:12):

@Yury G. Kudryashov What's your reason for preferring the cancellative version?

#### Yury G. Kudryashov (Aug 20 2020 at 03:12):

Copy+paste from wrong line

Fixed.

#### Yury G. Kudryashov (Aug 20 2020 at 03:27):

I'm going to wait for an answer before porting convex_on.

#### Frédéric Dupuis (Aug 20 2020 at 11:55):

I didn't have any particularly good reason -- at the beginning I was hoping it would allow us to define convexity for functions into things like nnreal, but as you say it doesn't work anyway. I'd be happy with just ordered_add_comm_group, it would clean things up a bit.

#### Frédéric Dupuis (Aug 20 2020 at 13:36):

Although now that I think about it, [ordered_semimodule nnreal β] might be useful for things like weighting Hermitian matrices by probabilities.

Last updated: May 06 2021 at 12:15 UTC