Zulip Chat Archive

Stream: new members

Topic: ordered_monoid?

Damiano Testa (Feb 11 2021 at 07:45):

Dear All,

is there a weaker instance than ordered_semiring that makes the lemma below true? It only talks about multiplication and order, but I could not find a class with which it works without assuming also an addition on R.

lemma ordered_monoid.one_le_mul {R : Type*} [ordered_semiring R] {a b : R}
  (a1 : 1  a) (b1 : 1  b) :
  (1 : R)  a * b :=
(mul_one (1 : R)).symm.le.trans (mul_le_mul a1 b1 zero_le_one (zero_le_one.trans a1))

Scott Morrison (Feb 11 2021 at 08:06):

I don't think we do.

Damiano Testa (Feb 11 2021 at 08:06):

(I should have said that I would like it to work when R is the real numbers)

Damiano Testa (Feb 11 2021 at 08:10):

Scott, thanks for looking into this! I may then PR this as is, close to mul_le_mul, probably.

Damiano Testa (Feb 11 2021 at 08:36):

PR #6172!

Last updated: Dec 20 2023 at 11:08 UTC