R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ (m : A), m ∈ ↑toSubmodule S → ∀ (n : A), n ∈ ↑toSubmodule T → m * n ∈ ↑toSubmodule (S ⊔ T)
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule T ≤ ↑toSubmodule (S ⊔ T)
rw [Submodule.mul_le]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ ↑toSubmodule (S ⊔ T)
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ (m : A), m ∈ ↑toSubmodule S → ∀ (n : A), n ∈ ↑toSubmodule T → m * n ∈ ↑toSubmodule (S ⊔ T)
intro y hy z hz
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ S ⊔ T
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ ↑toSubmodule (S ⊔ T)
show y * z ∈ S ⊔ T
no goals
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ S ⊔ T
exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)