eq_one_or_neg_one_of_mul_eq_neg_one'

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_neg_one' (h : u * v = -1) : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1 :=
  by
  obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1
  · exact Or.inl ⟨rfl, one_mul v ▸ h⟩
  · simpa [Int.neg_mul] using h

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