English
If G has IsLeftCancelMul, LinearOrder, and MulRightStrictMono, then TwoUniqueProds G.
Русский
Если G имеет IsLeftCancelMul, линейный порядок и правосторонняя строгая монотонность, то TwoUniqueProds G.
LaTeX
$$$ [\\text{IsLeftCancelMul }G][\\text{LinearOrder }G][\\text{MulRightStrictMono }G] \\Rightarrow \\mathrm{TwoUniqueProds} G. $$$
Lean4
/-- This instance asserts that if `G` has a left-cancellative multiplication, a linear order, and
multiplication is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueProds`. -/
@[to_additive /-- This instance asserts that if `G` has a left-cancellative addition, a linear order, and
addition is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueSums`. -/
]
instance (priority := 100) of_covariant_left [IsLeftCancelMul G] [LinearOrder G] [MulRightStrictMono G] :
TwoUniqueProds G :=
let _ := LinearOrder.lift' (unop : Gᵐᵒᵖ → G) unop_injective
let _ : MulLeftStrictMono Gᵐᵒᵖ := { elim := fun _ _ _ bc ↦ mul_lt_mul_right' (α := G) bc (unop _) }
of_mulOpposite of_covariant_right
