∀ (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],
  FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑1)⁻¹ * FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑1 = 1