haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ NoZeroSMulDivisors Rₚ Sₚ
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ