R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
⊢ Set.range ↑B.basis ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
⊢ adjoin R {B.gen} = ⊤
rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]
case intro
R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
i : Fin B.dim
⊢ ↑B.basis i ∈ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
⊢ Set.range ↑B.basis ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
rintro x ⟨i, rfl⟩
case intro
R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
i : Fin B.dim
⊢ B.gen ^ ↑i ∈ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
case intro
R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
i : Fin B.dim
⊢ ↑B.basis i ∈ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
rw [B.basis_eq_pow i]
no goals
case intro
R : Type u_1
S : Type u_2
T : Type ?u.713459
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.713762
B✝ : Type ?u.713765
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.714187
inst✝ : Field K
B : PowerBasis R S
i : Fin B.dim
⊢ B.gen ^ ↑i ∈ ↑(↑Subalgebra.toSubmodule (adjoin R {B.gen}))
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _