no goals
R : Type u_2
S : Type u_1
T : Type ?u.39838
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.40141
B : Type ?u.40144
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.40566
inst✝¹ : Field K
inst✝ : Nontrivial S
pb : PowerBasis R S
y : S
⊢ y ∈ Submodule.span R (Set.range fun i => pb.gen ^ ↑i)
simpa using pb.basis.mem_span y