isUnit_iff_norm_isUnit — Mathlib

English

An element z is a unit in Z[√d] if and only if z.norm is a unit in ℤ.

Русский

Элемент $z$ является единицей в $\\mathbb{Z}[\\sqrt{d}]$ тогда и только тогда, когда $z.noram$ является единицей в $\\mathbb{Z}$.

LaTeX

$$$\\text{IsUnit}(z) \\iff \\text{IsUnit}(z.norm)$$$

Lean4

theorem isUnit_iff_norm_isUnit {d : ℤ} (z : ℤ√d) : IsUnit z ↔ IsUnit z.norm := by
  rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]

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