{R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] → [inst_2 : Algebra R P] → FractionalIdeal S P → FractionalIdeal S P → FractionalIdeal S P