isUnit_iff — Mathlib

English

In the ring of integers of ℚ, every unit is either 1 or −1, i.e., the only units are ±1.

Русский

В кольце целых чисел ℚ единственными единицами являются ±1.

LaTeX

$$IsUnit(x) \iff x = 1 ∨ x = -1, \quad x ∈ 𝓞_{ℚ}$$

Lean4

theorem isUnit_iff {x : 𝓞 ℚ} : IsUnit x ↔ (x : ℚ) = 1 ∨ (x : ℚ) = -1 := by
  simp_rw [(isUnit_map_iff (Rat.ringOfIntegersEquiv : 𝓞 ℚ →+* ℤ) x).symm, Int.isUnit_iff, RingEquiv.coe_toRingHom,
    RingEquiv.map_eq_one_iff, RingEquiv.map_eq_neg_one_iff, ← Subtype.coe_injective.eq_iff];
  rfl

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