Scalar comparisons for ambiguous ideal classes have relative norm equal to a unit of the base ring. This formulation works directly with relative ideal norms, so it does not identify the unit obstruction with the trivial class.

theorem CCDN.ambiguous_numberField_ideal_norm_unit (F : Type u_3) (K : Type u_4) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] (σ : Gal(K/F)) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hI : (ClassGroup.mulEquiv (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv) (ClassGroup.mk0 I) = ClassGroup.mk0 I) : ∃ (x : NumberField.RingOfIntegers K) (y : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers F)ˣ), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * Ideal.map (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv.toRingHom ↑I = Ideal.span {y} * ↑I ∧ (Algebra.norm F) (↑y / ↑x) = ↑↑u

For number fields, the concrete scalar comparison has field norm equal to a base-field unit.