ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (map₂ (LinearMap.mul R A) M N).toAddSubmonoid =
    ⨆ (s : { x // x ∈ M.toAddSubmonoid }), AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
dsimp [HMul.hMul, Mul.mul]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (⨆ (i : { x // x ∈ M }), (map (↑(LinearMap.mul R A) ↑i) N).toAddSubmonoid) =
    ⨆ (s : { x // x ∈ M.toAddSubmonoid }), AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (map₂ (LinearMap.mul R A) M N).toAddSubmonoid =
    ⨆ (s : { x // x ∈ M.toAddSubmonoid }), AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
rw [map₂, iSup_toAddSubmonoid]
no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (⨆ (i : { x // x ∈ M }), (map (↑(LinearMap.mul R A) ↑i) N).toAddSubmonoid) =
    ⨆ (s : { x // x ∈ M.toAddSubmonoid }), AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
rfl