ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑Set.up {a} • span R ↑M = map (LinearMap.mulLeft R a) M
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑Set.up {a} • M = map (LinearMap.mulLeft R a) M
conv_lhs => rw [← span_eq M]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a})) * span R ↑M = map (LinearMap.mulLeft R a) M
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑Set.up {a} • span R ↑M = map (LinearMap.mulLeft R a) M
change span _ _ * span _ _ = _
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M) = map (LinearMap.mulLeft R a) M
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a})) * span R ↑M = map (LinearMap.mulLeft R a) M
rw [span_mul_span]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M) ≤ map (LinearMap.mulLeft R a) M

case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ map (LinearMap.mulLeft R a) M ≤ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M)
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M) = map (LinearMap.mulLeft R a) M
apply le_antisymm
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑SetSemiring.down (↑Set.up {a}) * ↑M ⊆ ↑(map (LinearMap.mulLeft R a) M)
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M) ≤ map (LinearMap.mulLeft R a) M
rw [span_le]
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
b m : A
hb : b ∈ ↑SetSemiring.down (↑Set.up {a})
hm : m ∈ ↑M
⊢ (fun x x_1 => x * x_1) b m ∈ ↑(map (LinearMap.mulLeft R a) M)
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑SetSemiring.down (↑Set.up {a}) * ↑M ⊆ ↑(map (LinearMap.mulLeft R a) M)
rintro _ ⟨b, m, hb, hm, rfl⟩
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
b m : A
hb : b ∈ ↑SetSemiring.down (↑Set.up {a})
hm : m ∈ ↑M
⊢ ∃ y, y ∈ M ∧ ↑(LinearMap.mulLeft R a) y = (fun x x_1 => x * x_1) a m
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
b m : A
hb : b ∈ ↑SetSemiring.down (↑Set.up {a})
hm : m ∈ ↑M
⊢ (fun x x_1 => x * x_1) b m ∈ ↑(map (LinearMap.mulLeft R a) M)
rw [SetLike.mem_coe, mem_map, Set.mem_singleton_iff.mp hb]
no goals
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
b m : A
hb : b ∈ ↑SetSemiring.down (↑Set.up {a})
hm : m ∈ ↑M
⊢ ∃ y, y ∈ M ∧ ↑(LinearMap.mulLeft R a) y = (fun x x_1 => x * x_1) a m
exact ⟨m, hm, rfl⟩
case a.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
m : A
hm : m ∈ ↑M
⊢ ↑(LinearMap.mulLeft R a) m ∈ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M)
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ map (LinearMap.mulLeft R a) M ≤ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M)
rintro _ ⟨m, hm, rfl⟩
no goals
case a.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
m : A
hm : m ∈ ↑M
⊢ ↑(LinearMap.mulLeft R a) m ∈ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M)
exact subset_span ⟨a, m, Set.mem_singleton a, hm, rfl⟩