R : Type u_1
A : Type u_2
B : Type ?u.694032
S : Type ?u.694035
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
hx : IsIntegral R x
⊢ {x} ⊆ ↑(integralClosure R A)
R : Type u_1
A : Type u_2
B : Type ?u.694032
S : Type ?u.694035
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
hx : IsIntegral R x
⊢ Algebra.adjoin R {x} ≤ integralClosure R A
rw [Algebra.adjoin_le_iff]
R : Type u_1
A : Type u_2
B : Type ?u.694032
S : Type ?u.694035
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
hx : IsIntegral R x
⊢ x ∈ integralClosure R A
R : Type u_1
A : Type u_2
B : Type ?u.694032
S : Type ?u.694035
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
hx : IsIntegral R x
⊢ {x} ⊆ ↑(integralClosure R A)
simp only [SetLike.mem_coe, Set.singleton_subset_iff]
no goals
R : Type u_1
A : Type u_2
B : Type ?u.694032
S : Type ?u.694035
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
hx : IsIntegral R x
⊢ x ∈ integralClosure R A
exact hx