English
For any x, natAbs(norm(x)) = 1 if and only if x is a unit.
Русский
Для любого $x$ natAbs нормы равна 1 тогда и только тогда, когда $x$ единица.
LaTeX
$$$\\operatorname{natAbs}(\\operatorname{norm}(x)) = 1 \\iff \\ IsUnit(x)$$$
Lean4
theorem norm_eq_one_iff {x : ℤ√d} : x.norm.natAbs = 1 ↔ IsUnit x :=
⟨fun h =>
isUnit_iff_dvd_one.2 <|
(le_total 0 (norm x)).casesOn
(fun hx =>
⟨star x, by
rwa [← Int.natCast_inj, Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _, norm_eq_mul_conj,
eq_comm] at h⟩)
fun hx =>
⟨-star x, by
rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _, Int.cast_neg,
norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h⟩,
fun h => by
let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
have := congr_arg (Int.natAbs ∘ norm) hy
rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one, Int.natAbs_one, eq_comm,
mul_eq_one] at this
exact this.1⟩
