R : Type u_1
A : Type u
B : Type ?u.8031
M : Type ?u.8034
N : Type ?u.8037
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ adjoin R {X} = ⊤
R : Type u_1
A : Type u
B : Type ?u.8031
M : Type ?u.8034
N : Type ?u.8037
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ adjoin R ↑{X} = ⊤
rw [Finset.coe_singleton]
no goals
R : Type u_1
A : Type u
B : Type ?u.8031
M : Type ?u.8034
N : Type ?u.8037
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ adjoin R {X} = ⊤
exact Polynomial.adjoin_X