feat: port NumberTheory.NumberField.Units (#5359)

Mathlib.lean

@@ -2307,6 +2307,7 @@ import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
 import Mathlib.NumberTheory.Multiplicity
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.NumberTheory.NumberField.Norm
+import Mathlib.NumberTheory.NumberField.Units
 import Mathlib.NumberTheory.Padics.Hensel
 import Mathlib.NumberTheory.Padics.PadicIntegers
 import Mathlib.NumberTheory.Padics.PadicNorm

Mathlib/NumberTheory/NumberField/Units.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2023 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+
+! This file was ported from Lean 3 source module number_theory.number_field.units
+! leanprover-community/mathlib commit 00f91228655eecdcd3ac97a7fd8dbcb139fe990a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.NumberTheory.NumberField.Norm
+
+/-!
+# Units of a number field
+We prove results about the group `(𝓞 K)ˣ` of units of the ring of integers `𝓞 K` of a number
+field `K`.
+
+## Main results
+* `isUnit_iff_norm`: an algebraic integer `x : 𝓞 K` is a unit if and only if `|norm ℚ x| = 1`
+
+## Tags
+number field, units
+ -/
+
+
+open scoped NumberField
+
+noncomputable section
+
+open NumberField Units
+
+section Rat
+
+theorem Rat.RingOfIntegers.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
+#align rat.ring_of_integers.is_unit_iff Rat.RingOfIntegers.isUnit_iff
+
+end Rat
+
+variable (K : Type _) [Field K]
+
+section IsUnit
+
+attribute [local instance] NumberField.ringOfIntegersAlgebra
+
+variable {K}
+
+theorem isUnit_iff_norm [NumberField K] (x : 𝓞 K) :
+    IsUnit x ↔ |(RingOfIntegers.norm ℚ x : ℚ)| = 1 := by
+  convert (RingOfIntegers.isUnit_norm ℚ (F := K)).symm
+  rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]
+#align is_unit_iff_norm isUnit_iff_norm
+
+end IsUnit