(K : Type u_3) →
  [inst : Field K] →
    {R₁ : Type u_4} →
      [inst_1 : CommRing R₁] →
        [IsDomain R₁] → [inst_3 : Algebra R₁ K] → [IsFractionRing R₁ K] → Inv (FractionalIdeal (nonZeroDivisors R₁) K)