R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Submodule.FG ⊤
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑s ⊆ ↑(↑toSubmodule (Algebra.adjoin R ↑s))
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Submodule.FG ⊤
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑toSubmodule (Algebra.adjoin R ↑s) = ↑toSubmodule ⊤
rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Submodule.FG ⊤
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑s ⊆ ↑(↑toSubmodule (Algebra.adjoin R ↑s))
exact Algebra.subset_adjoin