ordered_monoid?

Stream: new members

[Damiano Testa]

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]

I don't think we do.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

PR #6172!