trichotomy_of_mul_eq_mul — Mathlib

English

If a mixture of left and right strict monotone multiplications holds equality a·b = c·d, then either a=c and b=d, or a<c, or b<d.

Русский

Если выполнено равенство умножения при условиях левой и правой строгой монотонности, то либо a=c и b=d, либо a<c, либо b<d.

LaTeX

$$$$ \\forall a,b,c,d \\in \\alpha,\n a \\cdot b = c \\cdot d \\Rightarrow (a=c \\land b=d) \\lor a

Lean4

@[to_additive]
theorem trichotomy_of_mul_eq_mul [MulLeftStrictMono α] [MulRightStrictMono α] (h : a * b = c * d) :
    (a = c ∧ b = d) ∨ a < c ∨ b < d :=
  by
  obtain hac | rfl | hca := lt_trichotomy a c
  · grind
  · left; simpa using mul_right_inj_of_comparable (LinearOrder.le_total d b) |>.1 h
  · obtain hbd | rfl | hdb := lt_trichotomy b d
    · grind
    · exact False.elim <| ne_of_lt (mul_lt_mul_right' hca b) h.symm
    · exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

Похожие утверждения