mathlib3

00f91228 - feat(number_theory/number_field/units): add is_unit_iff_norm (#18866)

feat(number_theory/number_field/units): add is_unit_iff_norm (#18866) This PR creates the file `number_theory/number_field/units.lean` and proves the result : ```lean lemma is_unit_iff_norm [number_field K] (x : 𝓞 K) : is_unit x ↔ abs (ring_of_integers.norm ℚ x : ℚ) = 1 ```