{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {x : S} →
            {I : Ideal R} →
              [IsDomain R] →
                [IsIntegrallyClosed R] →
                  [IsDedekindDomain S] →
                    [Module.IsTorsionFree R S] →
                      Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
                        IsIntegral R x →
                          S ⧸ Ideal.map (algebraMap R S) I ≃+*
                            Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}