R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ Algebra.adjoin R {X}
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
⊢ Algebra.adjoin R {X} = ⊤
refine' top_unique fun p _hp => _
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ p ∈ S
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ Algebra.adjoin R {X}
set S := Algebra.adjoin R ({X} : Set R[X])
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (sum p fun n a => ↑(monomial n) a) ∈ S
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ p ∈ S
rw [← sum_monomial_eq p]
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (sum p fun n a => a • X ^ n) ∈ Algebra.adjoin R {X}
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (sum p fun n a => ↑(monomial n) a) ∈ S
simp only [← smul_X_eq_monomial, Sum]
no goals
R : Type u
S✝ : Type v
T : Type w
A : Type z
A' : Type ?u.422492
B' : Type ?u.422495
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.422708
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (sum p fun n a => a • X ^ n) ∈ Algebra.adjoin R {X}
exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (Algebra.subset_adjoin rfl) _) _