F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : Submodule.span F ↑b = ⊤
⊢ ↑b ⊆ ↑(Submodule.restrictScalars F (Submodule.span K ↑b))
F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : Submodule.span F ↑b = ⊤
⊢ Submodule.restrictScalars F (Submodule.span K ↑b) = Submodule.restrictScalars F ⊤
rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
no goals
F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : Submodule.span F ↑b = ⊤
⊢ ↑b ⊆ ↑(Submodule.restrictScalars F (Submodule.span K ↑b))
exact Submodule.subset_span