eq_one_or_neg_one_of_mul_eq_one' — Mathlib

English

If u · v = 1, then u = 1 ∧ v = 1 or u = -1 ∧ v = -1.

Русский

Если u · v = 1, тогда u = 1 и v = 1 или u = -1 и v = -1.

LaTeX

$$$ u v = 1 \Rightarrow (u = 1 \land v = 1) \lor (u = -1 \land v = -1)$$$

Lean4

theorem eq_one_or_neg_one_of_mul_eq_one' (h : u * v = 1) : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1 :=
  by
  have h' : v * u = 1 := mul_comm u v ▸ h
  obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h <;> obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h' <;>
    tauto

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