R : Type u_1
inst✝⁹ : CommRing R
S : Type ?u.516571
inst✝⁸ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝⁷ : Algebra R S
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A S
inst✝³ : IsScalarTower R A S
inst✝² : IsIntegralClosure A R S
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥
R : Type u_1
inst✝⁹ : CommRing R
S : Type ?u.516571
inst✝⁸ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝⁷ : Algebra R S
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A S
inst✝³ : IsScalarTower R A S
inst✝² : IsIntegralClosure A R S
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ comap (algebraMap R A) I = ⊥ → I = ⊥
contrapose
no goals
R : Type u_1
inst✝⁹ : CommRing R
S : Type ?u.516571
inst✝⁸ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝⁷ : Algebra R S
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A S
inst✝³ : IsScalarTower R A S
inst✝² : IsIntegralClosure A R S
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥
exact (IsIntegralClosure.comap_ne_bot S)