∀ (R : Type u_2) (K : Type u_1) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] (x y : Kˣ),
  { val := FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑(x * y),
      inv := FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑(x * y))⁻¹, val_inv := ⋯, inv_val := ⋯ } =
    { val := FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x,
        inv := FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ } *
      { val := FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑y,
        inv := FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑y)⁻¹, val_inv := ⋯, inv_val := ⋯ }