case a
ι : 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
⊢ map (↑(opLinearEquiv R)) (M * N) ≤ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M

case a
ι : 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
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)
ι : 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
⊢ map (↑(opLinearEquiv R)) (M * N) = map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
apply le_antisymm
case a
ι : 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 ≤ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)
case a
ι : 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
⊢ map (↑(opLinearEquiv R)) (M * N) ≤ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
simp_rw [map_le_iff_le_comap]
case a
ι : 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✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ m * n ∈ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)
case a
ι : 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 ≤ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)
refine' mul_le.2 fun m hm n hn => _
case a
ι : 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✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑↑(opLinearEquiv R) (m * n) ∈
    comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
case a
ι : 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✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ m * n ∈ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)
rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
case a
ι : 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✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ op n * op m ∈ comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
case a
ι : 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✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑↑(opLinearEquiv R) (m * n) ∈
    comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
show op n * op m ∈ _
no goals
case a
ι : 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✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ op n * op m ∈ comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
exact mul_mem_mul hn hm
case a
ι : 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✝ m : A
hm : op m ∈ map (↑(opLinearEquiv R)) N
n : A
hn : op n ∈ map (↑(opLinearEquiv R)) M
⊢ op m * op n ∈ map (↑(opLinearEquiv R)) (M * N)
case a
ι : 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
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)
refine' mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => _)
case a
ι : 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✝ m : A
hm : ↑(LinearEquiv.symm (opLinearEquiv R)) (op m) ∈ N
n : A
hn : ↑(LinearEquiv.symm (opLinearEquiv R)) (op n) ∈ M
⊢ ↑(LinearEquiv.symm (opLinearEquiv R)) (op m * op n) ∈ M * N
case a
ι : 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✝ m : A
hm : op m ∈ map (↑(opLinearEquiv R)) N
n : A
hn : op n ∈ map (↑(opLinearEquiv R)) M
⊢ op m * op n ∈ map (↑(opLinearEquiv R)) (M * N)
rw [Submodule.mem_map_equiv] at hm hn⊢
no goals
case a
ι : 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✝ m : A
hm : ↑(LinearEquiv.symm (opLinearEquiv R)) (op m) ∈ N
n : A
hn : ↑(LinearEquiv.symm (opLinearEquiv R)) (op n) ∈ M
⊢ ↑(LinearEquiv.symm (opLinearEquiv R)) (op m * op n) ∈ M * N
exact mul_mem_mul hn hm