Stuff for Mathlib.Algebra.Order.Monoid.Unbundled.Basic #
theorem
MulLECancellable.hMul
{α : Type u_1}
[LE α]
[Semigroup α]
{a b : α}
(ha : MulLECancellable a)
(hb : MulLECancellable b)
:
MulLECancellable (a * b)
theorem
AddLECancellable.hAdd
{α : Type u_1}
[LE α]
[AddSemigroup α]
{a b : α}
(ha : AddLECancellable a)
(hb : AddLECancellable b)
:
AddLECancellable (a + b)
theorem
MulLECancellable.of_hMul_left
{α : Type u_1}
[LE α]
[Semigroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
{a b : α}
(hab : MulLECancellable (a * b))
:
theorem
AddLECancellable.of_hAdd_left
{α : Type u_1}
[LE α]
[AddSemigroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
{a b : α}
(hab : AddLECancellable (a + b))
: