mul_eq_neg_one_iff_eq_one_or_neg_one

English

For units u,v in ℤ, u·v = -1 iff u = 1 ∧ v = -1 or u = -1 ∧ v = 1.

Русский

Для единиц u,v в ℤ, u·v = -1 тогда, когда u = 1 и v = -1 или u = -1 и v = 1.

LaTeX

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

Lean4

theorem mul_eq_neg_one_iff_eq_one_or_neg_one : u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1 := by
  refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
      obtain ⟨rfl, rfl⟩ := H <;>
    rfl

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