isUnit_iff — Mathlib

English

A number u is a unit in ℤ if and only if u is either 1 or -1.

Русский

Число u является единицей в ℤ тогда и только тогда, когда u = 1 или u = -1.

LaTeX

$$$ \text{IsUnit}(u) \iff (u = 1 \lor u = -1)$$$

Lean4

theorem isUnit_iff : IsUnit u ↔ u = 1 ∨ u = -1 :=
  by
  refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩
  rcases h with (rfl | rfl)
  · exact isUnit_one
  · exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

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