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
S : Subalgebra R A
x✝ : Submodule.FG (↑toSubmodule S)
t : Finset A
ht : span R ↑t = ↑toSubmodule S
x : A
hx : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule 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
S : Subalgebra R A
x✝ : Submodule.FG (↑toSubmodule S)
t : Finset A
ht : span R ↑t = ↑toSubmodule S
x : A
hx : x ∈ ↑toSubmodule S
⊢ x ∈ span R ↑t
rw [ht]
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
S : Subalgebra R A
x✝ : Submodule.FG (↑toSubmodule S)
t : Finset A
ht : span R ↑t = ↑toSubmodule S
x : A
hx : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule S
exact hx