English
Pull back an IsOrderedCancelMonoid via a strictly monotone map; the resulting β has ordered cancellative properties.
Русский
Переносим IsOrderedCancelMonoid через строго монотонное отображение; β наследует упорядоченную отменяемость.
LaTeX
$$$\\text{IsOrderedCancelMonoid}(\\beta)$ via \\text{StrictMono}$$
Lean4
/-- Pullback an `IsOrderedCancelMonoid` under a strictly monotone map. -/
@[to_additive /-- Pullback an `IsOrderedAddCancelMonoid` under a strictly monotone map. -/
]
theorem isOrderedCancelMonoid [IsOrderedCancelMonoid α] [CommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f)
(mul : ∀ x y, f (x * y) = f x * f y) : IsOrderedCancelMonoid β
where
__ := hf.isOrderedMonoid f mul
le_of_mul_le_mul_left a b c h := by simpa [← hf.le_iff_le, mul] using h
