mathlib documentation

linear_algebra.basic

Linear algebra

This file defines the basics of linear algebra. It sets up the "categorical/lattice structure" of modules over a ring, submodules, and linear maps. If p and q are submodules of a module, p ≤ q means that p ⊆ q.

Many of the relevant definitions, including module, submodule, and linear_map, are found in src/algebra/module.

Main definitions

Main statements

Notations

Implementation notes

We note that, when constructing linear maps, it is convenient to use operations defined on bundled maps (prod, coprod, arithmetic operations like +) instead of defining a function and proving it is linear.

Tags

linear algebra, vector space, module

theorem finsupp.smul_sum {α : Type u} {β : Type v} {R : Type w} {M : Type y} [has_zero β] [semiring R] [add_comm_monoid M] [semimodule R M] {v : α →₀ β} {c : R} {h : α → β → M} :
c v.sum h = v.sum (λ (a : α) (b : β), c h a b)

theorem pi_eq_sum_univ {ι : Type u} [fintype ι] {R : Type v} [semiring R] (x : ι → R) :
x = ∑ (i : ι), x i λ (j : ι), ite (i = j) 1 0

decomposing x : ι → R as a sum along the canonical basis

Properties of linear maps

@[simp]
theorem linear_map.comp_id {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

@[simp]
theorem linear_map.id_comp {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

theorem linear_map.comp_assoc {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (h : M₃ →ₗ[R] M₄) :
(h.comp g).comp f = h.comp (g.comp f)

def linear_map.dom_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (p : submodule R M) :
p →ₗ[R] M₂

The restriction of a linear map f : M → M₂ to a submodule p ⊆ M gives a linear map p → M₂.

Equations
@[simp]
theorem linear_map.dom_restrict_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (p : submodule R M) (x : p) :

def linear_map.cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M₂ →ₗ[R] M) :
(∀ (c : M₂), f c p)(M₂ →ₗ[R] p)

A linear map f : M₂ → M whose values lie in a submodule p ⊆ M can be restricted to a linear map M₂ → p.

Equations
@[simp]
theorem linear_map.cod_restrict_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M₂ →ₗ[R] M) {h : ∀ (c : M₂), f c p} (x : M₂) :

@[simp]
theorem linear_map.comp_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (p : submodule R M₂) (h : ∀ (b : M), f b p) (g : M₃ →ₗ[R] M) :

@[simp]
theorem linear_map.subtype_comp_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (p : submodule R M₂) (h : ∀ (b : M), f b p) :

def linear_map.restrict {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) {p : submodule R M} :
(∀ (x : M), x pf x p)(p →ₗ[R] p)

Restrict domain and codomain of an endomorphism.

Equations
theorem linear_map.restrict_apply {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), x pf x p) (x : p) :
(f.restrict hf) x = f x, _⟩

theorem linear_map.subtype_comp_restrict {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), x pf x p) :

theorem linear_map.restrict_eq_cod_restrict_dom_restrict {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), x pf x p) :

theorem linear_map.restrict_eq_dom_restrict_cod_restrict {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), f x p) :

@[instance]
def linear_map.has_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_zero (M →ₗ[R] M₂)

The constant 0 map is linear.

Equations
@[instance]
def linear_map.inhabited {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

Equations
@[simp]
theorem linear_map.zero_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M) :
0 x = 0

@[simp]
theorem linear_map.default_def {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
default (M →ₗ[R] M₂) = 0

@[instance]
def linear_map.unique_of_left {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [subsingleton M] :
unique (M →ₗ[R] M₂)

Equations
@[instance]
def linear_map.unique_of_right {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [subsingleton M₂] :
unique (M →ₗ[R] M₂)

Equations
@[instance]
def linear_map.has_add {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_add (M →ₗ[R] M₂)

The sum of two linear maps is linear.

Equations
@[simp]
theorem linear_map.add_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f g : M →ₗ[R] M₂) (x : M) :
(f + g) x = f x + g x

@[instance]
def linear_map.add_comm_monoid {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

The type of linear maps is an additive monoid.

Equations
@[instance]
def linear_map.linear_map_apply_is_add_monoid_hom {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (a : M) :
is_add_monoid_hom (λ (f : M →ₗ[R] M₂), f a)

theorem linear_map.add_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g h : M₂ →ₗ[R] M₃) :
(h + g).comp f = h.comp f + g.comp f

theorem linear_map.comp_add {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f g : M →ₗ[R] M₂) (h : M₂ →ₗ[R] M₃) :
h.comp (f + g) = h.comp f + h.comp g

theorem linear_map.sum_apply {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (t : finset ι) (f : ι → (M →ₗ[R] M₂)) (b : M) :
(∑ (d : ι) in t, f d) b = ∑ (d : ι) in t, (f d) b

def linear_map.smul_right {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M₂ →ₗ[R] R)M → (M₂ →ₗ[R] M)

λb, f b • x is a linear map.

Equations
@[simp]
theorem linear_map.smul_right_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
(f.smul_right x) c = f c x

@[instance]
def linear_map.has_one {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def linear_map.has_mul {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[simp]
theorem linear_map.one_app {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :
1 x = x

@[simp]
theorem linear_map.mul_app {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (A B : M →ₗ[R] M) (x : M) :
(A * B) x = A (B x)

@[simp]
theorem linear_map.comp_zero {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) :
f.comp 0 = 0

@[simp]
theorem linear_map.zero_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) :
0.comp f = 0

theorem linear_map.coe_fn_sum {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {ι : Type u_1} (t : finset ι) (f : ι → (M →ₗ[R] M₂)) :
∑ (i : ι) in t, f i = ∑ (i : ι) in t, (f i)

@[instance]
def linear_map.monoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
theorem linear_map.pi_apply_eq_sum_univ {R : Type u} {M : Type v} {ι : Type x} [semiring R] [add_comm_monoid M] [semimodule R M] [fintype ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
f x = ∑ (i : ι), x i f (λ (j : ι), ite (i = j) 1 0)

A linear map f applied to x : ι → R can be computed using the image under f of elements of the canonical basis.

def linear_map.fst (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
M × M₂ →ₗ[R] M

The first projection of a product is a linear map.

Equations
def linear_map.snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
M × M₂ →ₗ[R] M₂

The second projection of a product is a linear map.

Equations
@[simp]
theorem linear_map.fst_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M × M₂) :
(linear_map.fst R M M₂) x = x.fst

@[simp]
theorem linear_map.snd_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M × M₂) :
(linear_map.snd R M M₂) x = x.snd

def linear_map.prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] :
(M →ₗ[R] M₂)(M →ₗ[R] M₃)(M →ₗ[R] M₂ × M₃)

The prod of two linear maps is a linear map.

Equations
@[simp]
theorem linear_map.prod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (x : M) :
(f.prod g) x = (f x, g x)

@[simp]
theorem linear_map.fst_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
(linear_map.fst R M₂ M₃).comp (f.prod g) = f

@[simp]
theorem linear_map.snd_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
(linear_map.snd R M₂ M₃).comp (f.prod g) = g

@[simp]
theorem linear_map.pair_fst_snd {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

def linear_map.inl (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
M →ₗ[R] M × M₂

The left injection into a product is a linear map.

Equations
def linear_map.inr (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
M₂ →ₗ[R] M × M₂

The right injection into a product is a linear map.

Equations
@[simp]
theorem linear_map.inl_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M) :
(linear_map.inl R M M₂) x = (x, 0)

@[simp]
theorem linear_map.inr_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M₂) :
(linear_map.inr R M M₂) x = (0, x)

theorem linear_map.inl_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.inr_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

def linear_map.coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] :
(M →ₗ[R] M₃)(M₂ →ₗ[R] M₃)(M × M₂ →ₗ[R] M₃)

The coprod function λ x : M × M₂, f x.1 + g x.2 is a linear map.

Equations
@[simp]
theorem linear_map.coprod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (x : M) (y : M₂) :
(f.coprod g) (x, y) = f x + g y

@[simp]
theorem linear_map.coprod_inl {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
(f.coprod g).comp (linear_map.inl R M M₂) = f

@[simp]
theorem linear_map.coprod_inr {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
(f.coprod g).comp (linear_map.inr R M M₂) = g

@[simp]
theorem linear_map.coprod_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.fst_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.snd_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.inl_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.inr_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

def linear_map.prod_map {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] :
(M →ₗ[R] M₃)(M₂ →ₗ[R] M₄)(M × M₂ →ₗ[R] M₃ × M₄)

prod.map of two linear maps.

Equations
@[simp]
theorem linear_map.prod_map_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x : M × M₂) :
(f.prod_map g) x = (f x.fst, g x.snd)

@[instance]
def linear_map.has_neg {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] :
has_neg (M →ₗ[R] M₂)

The negation of a linear map is linear.

Equations
@[simp]
theorem linear_map.neg_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (x : M) :
(-f) x = -f x

@[simp]
theorem linear_map.comp_neg {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [add_comm_group M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
g.comp (-f) = -g.comp f

@[instance]
def linear_map.add_comm_group {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] :

The type of linear maps is an additive group.

Equations
@[instance]
def linear_map.linear_map_apply_is_add_group_hom {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (a : M) :
is_add_group_hom (λ (f : M →ₗ[R] M₂), f a)

@[simp]
theorem linear_map.sub_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f g : M →ₗ[R] M₂) (x : M) :
(f - g) x = f x - g x

theorem linear_map.sub_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [add_comm_group M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g h : M₂ →ₗ[R] M₃) :
(g - h).comp f = g.comp f - h.comp f

theorem linear_map.comp_sub {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_group M₂] [add_comm_group M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f g : M →ₗ[R] M₂) (h : M₂ →ₗ[R] M₃) :
h.comp (g - f) = h.comp g - h.comp f

@[instance]
def linear_map.has_scalar {R : Type u} {M : Type v} {M₂ : Type w} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_scalar R (M →ₗ[R] M₂)

Equations
@[simp]
theorem linear_map.smul_apply {R : Type u} {M : Type v} {M₂ : Type w} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (a : R) (x : M) :
(a f) x = a f x

@[instance]
def linear_map.semimodule {R : Type u} {M : Type v} {M₂ : Type w} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
semimodule R (M →ₗ[R] M₂)

Equations
def linear_map.comp_right {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] :
(M₂ →ₗ[R] M₃)((M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃)

Composition by f : M₂ → M₃ is a linear map from the space of linear maps M → M₂ to the space of linear maps M₂ → M₃.

Equations
theorem linear_map.smul_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (a : R) :
(a g).comp f = a g.comp f

theorem linear_map.comp_smul {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (a : R) :
g.comp (a f) = a g.comp f

def linear_map.applyₗ {R : Type u} {M : Type v} {M₂ : Type w} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
M → ((M →ₗ[R] M₂) →ₗ[R] M₂)

Applying a linear map at v : M, seen as a linear map from M →ₗ[R] M₂ to M₂.

Equations
theorem linear_map.mul_apply {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (f g : M →ₗ[R] M) (x : M) :
(f * g) x = f (g x)

def linear_map.smul_rightₗ {R : Type u} {M : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] :
(M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M

The family of linear maps M₂ → M parameterised by f ∈ M₂ → R, x ∈ M, is linear in f, x.

Equations
@[simp]
theorem linear_map.smul_rightₗ_apply {R : Type u} {M : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :

Properties of submodules

@[instance]
def submodule.partial_order {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
theorem submodule.le_def {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
p p' p p'

theorem submodule.le_def' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
p p' ∀ (x : M), x px p'

theorem submodule.lt_def {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
p < p' p p'

theorem submodule.not_le_iff_exists {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
¬p p' ∃ (x : M) (H : x p), x p'

theorem submodule.exists_of_lt {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
p < p'(∃ (x : M) (H : x p'), x p)

theorem submodule.lt_iff_le_and_exists {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
p < p' p p' ∃ (x : M) (H : x p'), x p

def submodule.of_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
p p'(p →ₗ[R] p')

If two submodules p and p' satisfy p ⊆ p', then of_le p p' is the linear map version of this inclusion.

Equations
@[simp]
theorem submodule.coe_of_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} (h : p p') (x : p) :

theorem submodule.of_le_apply {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} (h : p p') (x : p) :

theorem submodule.subtype_comp_of_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p q : submodule R M) (h : p q) :

@[instance]
def submodule.has_bot {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

The set {0} is the bottom element of the lattice of submodules.

Equations
@[instance]
def submodule.inhabited' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[simp]
theorem submodule.bot_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :
= {0}

@[simp]
theorem submodule.mem_bot (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} :
x x = 0

theorem submodule.nonzero_mem_of_bot_lt {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {I : submodule R M} :
< I(∃ (a : I), a 0)

theorem submodule.eq_bot_iff {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :
p = ∀ (x : M), x px = 0

theorem submodule.ne_bot_iff {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :
p ∃ (x : M) (H : x p), x 0

@[instance]
def submodule.has_top {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

The universal set is the top element of the lattice of submodules.

Equations
@[simp]
theorem submodule.top_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem submodule.mem_top {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} :

theorem submodule.eq_bot_of_zero_eq_one {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :
0 = 1p =

@[instance]
def submodule.has_Inf {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def submodule.has_inf {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def submodule.complete_lattice {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[simp]
theorem submodule.add_eq_sup {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p q : submodule R M) :
p + q = p q

@[simp]
theorem submodule.zero_eq_bot {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :
0 =

theorem submodule.eq_top_iff' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p : submodule R M} :
p = ∀ (x : M), x p

theorem submodule.bot_ne_top {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] [nontrivial M] :

@[simp]
theorem submodule.inf_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p p' : submodule R M) :

@[simp]
theorem submodule.mem_inf {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} {p p' : submodule R M} :
x p p' x p x p'

@[simp]
theorem submodule.Inf_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (P : set (submodule R M)) :
(Inf P) = ⋂ (p : submodule R M) (H : p P), p

@[simp]
theorem submodule.infi_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort u_1} (p : ι → submodule R M) :
(⨅ (i : ι), p i) = ⋂ (i : ι), (p i)

@[simp]
theorem submodule.mem_Inf {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {S : set (submodule R M)} {x : M} :
x Inf S ∀ (p : submodule R M), p Sx p

@[simp]
theorem submodule.mem_infi {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} {ι : Sort u_1} (p : ι → submodule R M) :
(x ⨅ (i : ι), p i) ∀ (i : ι), x p i

theorem submodule.disjoint_def {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
disjoint p p' ∀ (x : M), x px p'x = 0

theorem submodule.disjoint_def' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} :
disjoint p p' ∀ (x : M), x p∀ (y : M), y p'x = yx = 0

theorem submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} (h : disjoint p p') {x : p} :
x p' x = 0

theorem submodule.mem_left_iff_eq_zero_of_disjoint {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} (h : disjoint p p') {x : p'} :
x p x = 0

def submodule.map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →ₗ[R] M₂)submodule R Msubmodule R M₂

The pushforward of a submodule p ⊆ M by f : M → M₂

Equations
@[simp]
theorem submodule.map_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (p : submodule R M) :

@[simp]
theorem submodule.mem_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} {x : M₂} :
x submodule.map f p ∃ (y : M), y p f y = x

theorem submodule.mem_map_of_mem {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} {r : M} :
r pf r submodule.map f p

@[simp]
theorem submodule.map_id {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :

theorem submodule.map_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : submodule R M) :

theorem submodule.map_mono {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p p' : submodule R M} :

@[simp]
theorem submodule.map_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) :

def submodule.comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →ₗ[R] M₂)submodule R M₂submodule R M

The pullback of a submodule p ⊆ M₂ along f : M → M₂

Equations
@[simp]
theorem submodule.comap_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (p : submodule R M₂) :

@[simp]
theorem submodule.mem_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {x : M} {f : M →ₗ[R] M₂} {p : submodule R M₂} :

theorem submodule.comap_id {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :

theorem submodule.comap_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : submodule R M₃) :

theorem submodule.comap_mono {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {q q' : submodule R M₂} :

theorem submodule.map_le_iff_le_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} {q : submodule R M₂} :

theorem submodule.gc_map_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

@[simp]
theorem submodule.map_bot {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

@[simp]
theorem submodule.map_sup {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p p' : submodule R M) (f : M →ₗ[R] M₂) :

@[simp]
theorem submodule.map_supr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {ι : Sort u_1} (f : M →ₗ[R] M₂) (p : ι → submodule R M) :
submodule.map f (⨆ (i : ι), p i) = ⨆ (i : ι), submodule.map f (p i)

@[simp]
theorem submodule.comap_top {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

@[simp]
theorem submodule.comap_inf {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (q q' : submodule R M₂) (f : M →ₗ[R] M₂) :

@[simp]
theorem submodule.comap_infi {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {ι : Sort u_1} (f : M →ₗ[R] M₂) (p : ι → submodule R M₂) :
submodule.comap f (⨅ (i : ι), p i) = ⨅ (i : ι), submodule.comap f (p i)

@[simp]
theorem submodule.comap_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (q : submodule R M₂) :

theorem submodule.map_comap_le {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (q : submodule R M₂) :

theorem submodule.le_comap_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (p : submodule R M) :

theorem submodule.map_inf_eq_map_inf_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} {p' : submodule R M₂} :

theorem submodule.map_comap_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p p' : submodule R M) :

theorem submodule.eq_zero_of_bot_submodule {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (b : ) :
b = 0

def submodule.span (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :
set Msubmodule R M

The span of a set s ⊆ M is the smallest submodule of M that contains s.

Equations
theorem submodule.mem_span {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} {s : set M} :
x submodule.span R s ∀ (p : submodule R M), s px p

theorem submodule.subset_span {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} :

theorem submodule.span_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} {p : submodule R M} :

theorem submodule.span_mono {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s t : set M} :

theorem submodule.span_eq_of_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) {s : set M} :
s pp submodule.span R ssubmodule.span R s = p

@[simp]
theorem submodule.span_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :

theorem submodule.map_span {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (s : set M) :

theorem submodule.span_induction {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} {s : set M} {p : M → Prop} :
x submodule.span R s(∀ (x : M), x sp x)p 0(∀ (x y : M), p xp yp (x + y))(∀ (a : R) (x : M), p xp (a x))p x

An induction principle for span membership. If p holds for 0 and all elements of s, and is preserved under addition and scalar multiplication, then p holds for all elements of the span of s.

def submodule.gi (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] :

span forms a Galois insertion with the coercion from submodule to set.

Equations
@[simp]
theorem submodule.span_empty {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem submodule.span_univ {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

theorem submodule.span_union {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (s t : set M) :

theorem submodule.span_Union {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort u_1} (s : ι → set M) :
submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), submodule.span R (s i)

@[simp]
theorem submodule.coe_supr_of_directed {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort u_1} [hι : nonempty ι] (S : ι → submodule R M) :
directed has_le.le S((supr S) = ⋃ (i : ι), (S i))

theorem submodule.mem_sup_left {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {S T : submodule R M} {x : M} :
x Sx S T

theorem submodule.mem_sup_right {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {S T : submodule R M} {x : M} :
x Tx S T

theorem submodule.mem_supr_of_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort u_1} {b : M} {p : ι → submodule R M} (i : ι) :
b p i(b ⨆ (i : ι), p i)

theorem submodule.mem_Sup_of_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {S : set (submodule R M)} {s : submodule R M} (hs : s S) {x : M} :
x sx Sup S

@[simp]
theorem submodule.mem_supr_of_directed {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort u_1} [nonempty ι] (S : ι → submodule R M) (H : directed has_le.le S) {x : M} :
x supr S ∃ (i : ι), x S i

theorem submodule.mem_Sup_of_directed {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set (submodule R M)} {z : M} :
s.nonemptydirected_on has_le.le s(z Sup s ∃ (y : submodule R M) (H : y s), z y)

theorem submodule.mem_sup {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} {x : M} :
x p p' ∃ (y : M) (H : y p) (z : M) (H : z p'), y + z = x

theorem submodule.mem_sup' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p p' : submodule R M} {x : M} :
x p p' ∃ (y : p) (z : p'), y + z = x

theorem submodule.mem_span_singleton_self {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :

theorem submodule.nontrivial_span_singleton {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} :

theorem submodule.mem_span_singleton {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x y : M} :
x submodule.span R {y} ∃ (a : R), a y = x

theorem submodule.le_span_singleton_iff {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s : submodule R M} {v₀ : M} :
s submodule.span R {v₀} ∀ (v : M), v s(∃ (r : R), r v₀ = v)

theorem submodule.span_singleton_eq_range {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (y : M) :
(submodule.span R {y}) = set.range (λ (_x : R), _x y)

theorem submodule.span_singleton_smul_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (r : R) (x : M) :

theorem submodule.span_singleton_smul_eq {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {r : K} (x : E) :
r 0submodule.span K {r x} = submodule.span K {x}

theorem submodule.disjoint_span_singleton {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {s : submodule K E} {x : E} :
disjoint s (submodule.span K {x}) x sx = 0

theorem submodule.disjoint_span_singleton' {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {p : submodule K E} {x : E} :
x 0(disjoint p (submodule.span K {x}) x p)

theorem submodule.mem_span_insert {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} {s : set M} {y : M} :
x submodule.span R (insert y s) ∃ (a : R) (z : M) (H : z submodule.span R s), x = a y + z

theorem submodule.span_insert_eq_span {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} {s : set M} :

theorem submodule.span_span {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} :

theorem submodule.span_eq_bot {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} :
submodule.span R s = ∀ (x : M), x sx = 0

@[simp]
theorem submodule.span_singleton_eq_bot {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {x : M} :

@[simp]
theorem submodule.span_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem submodule.span_image {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {s : set M} (f : M →ₗ[R] M₂) :

theorem submodule.supr_eq_span {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort w} (p : ι → submodule R M) :
(⨆ (i : ι), p i) = submodule.span R (⋃ (i : ι), (p i))

theorem submodule.span_singleton_le_iff_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (m : M) (p : submodule R M) :

theorem submodule.lt_add_iff_not_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {I : submodule R M} {a : M} :
I < I + submodule.span R {a} a I

theorem submodule.mem_supr {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Sort w} (p : ι → submodule R M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : submodule R M), (∀ (i : ι), p i N)m N

def submodule.prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
submodule R Msubmodule R M₂submodule R (M × M₂)

The product of two submodules is a submodule.

Equations
@[simp]
theorem submodule.prod_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (q : submodule R M₂) :
(p.prod q) = p.prod q

@[simp]
theorem submodule.mem_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {p : submodule R M} {q : submodule R M₂} {x : M × M₂} :
x p.prod q x.fst p x.snd q

theorem submodule.span_prod_le {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (s : set M) (t : set M₂) :

@[simp]
theorem submodule.prod_top {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem submodule.prod_bot {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem submodule.prod_mono {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {p p' : submodule R M} {q q' : submodule R M₂} :
p p'q q'p.prod q p'.prod q'

@[simp]
theorem submodule.prod_inf_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p p' : submodule R M) (q q' : submodule R M₂) :
p.prod q p'.prod q' = (p p').prod (q q')

@[simp]
theorem submodule.prod_sup_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p p' : submodule R M) (q q' : submodule R M₂) :
p.prod q p'.prod q' = (p p').prod (q q')

@[simp]
theorem submodule.neg_coe {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

@[simp]
theorem submodule.map_neg {R : Type u} {M : Type v} {M₂ : Type w} [ring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M →ₗ[R] M₂) :

@[simp]
theorem submodule.span_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (s : set M) :

theorem submodule.mem_span_insert' {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] {x y : M} {s : set M} :
x submodule.span R (insert y s) ∃ (a : R), x + a y submodule.span R s

def submodule.quotient_rel {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] :
submodule R Msetoid M

The equivalence relation associated to a submodule p, defined by x ≈ y iff y - x ∈ p.

Equations
def submodule.quotient {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] :
submodule R MType v

The quotient of a module M by a submodule p ⊆ M.

Equations
def submodule.quotient.mk {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] {p : submodule R M} :
M → p.quotient

Map associating to an element of M the corresponding element of M/p, when p is a submodule of M.

Equations
@[simp]
theorem submodule.quotient.mk_eq_mk {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] {p : submodule R M} (x : M) :

@[simp]
theorem submodule.quotient.mk'_eq_mk {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] {p : submodule R M} (x : M) :

@[simp]
theorem submodule.quotient.quot_mk_eq_mk {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] {p : submodule R M} (x : M) :

theorem submodule.quotient.eq {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) {x y : M} :

@[instance]
def submodule.quotient.has_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

Equations
@[instance]
def submodule.quotient.inhabited {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

Equations
@[simp]
theorem submodule.quotient.mk_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

@[simp]
theorem submodule.quotient.mk_eq_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) {x : M} :

@[instance]
def submodule.quotient.has_add {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

Equations
@[simp]
theorem submodule.quotient.mk_add {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) {x y : M} :

@[instance]
def submodule.quotient.has_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

Equations
@[simp]
theorem submodule.quotient.mk_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) {x : M} :

@[instance]
def submodule.quotient.has_scalar {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

Equations
@[simp]
theorem submodule.quotient.mk_smul {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) {r : R} {x : M} :

theorem submodule.quotient.nontrivial_of_lt_top {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : submodule R M) :

theorem submodule.quot_hom_ext {R : Type u} {M : Type v} {M₂ : Type w} [ring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) ⦃f g : p.quotient →ₗ[R] M₂⦄ :
(∀ (x : M), f (submodule.quotient.mk x) = g (submodule.quotient.mk x))f = g

theorem submodule.comap_smul {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [add_comm_group V] [vector_space K V] [add_comm_group V₂] [vector_space K V₂] (f : V →ₗ[K] V₂) (p : submodule K V₂) (a : K) :

theorem submodule.map_smul {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [add_comm_group V] [vector_space K V] [add_comm_group V₂] [vector_space K V₂] (f : V →ₗ[K] V₂) (p : submodule K V) (a : K) :
a 0submodule.map (a f) p = submodule.map f p

theorem submodule.comap_smul' {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [add_comm_group V] [vector_space K V] [add_comm_group V₂] [vector_space K V₂] (f : V →ₗ[K] V₂) (p : submodule K V₂) (a : K) :
submodule.comap (a f) p = ⨅ (h : a 0), submodule.comap f p

theorem submodule.map_smul' {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [add_comm_group V] [vector_space K V] [add_comm_group V₂] [vector_space K V₂] (f : V →ₗ[K] V₂) (p : submodule K V) (a : K) :
submodule.map (a f) p = ⨆ (h : a 0), submodule.map f p

Properties of linear maps

theorem linear_map.eq_on_span {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {s : set M} {f g : M →ₗ[R] M₂} (H : set.eq_on f g s) ⦃x : M⦄ :
x submodule.span R sf x = g x

If two linear maps are equal on a set s, then they are equal on submodule.span s.

See also linear_map.eq_on_span' for a version using set.eq_on.

theorem linear_map.eq_on_span' {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {s : set M} {f g : M →ₗ[R] M₂} :

If two linear maps are equal on a set s, then they are equal on submodule.span s.

This version uses set.eq_on, and the hidden argument will expand to h : x ∈ (span R s : set M). See linear_map.eq_on_span for a version that takes h : x ∈ span R s as an argument.

theorem linear_map.ext_on {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {s : set M} {f g : M →ₗ[R] M₂} :
submodule.span R s = set.eq_on f g sf = g

If s generates the whole semimodule and linear maps f, g are equal on s, then they are equal.

theorem linear_map.ext_on_range {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {v : ι → M} {f g : M →ₗ[R] M₂} :
submodule.span R (set.range v) = (∀ (i : ι), f (v i) = g (v i))f = g

If the range of v : ι → M generates the whole semimodule and linear maps f, g are equal at each v i, then they are equal.

@[simp]
theorem linear_map.finsupp_sum {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {γ : Type u_1} [has_zero γ] (f : M →ₗ[R] M₂) {t : ι →₀ γ} {g : ι → γ → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ), f (g i d))

theorem linear_map.map_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M₂ →ₗ[R] M) (h : ∀ (c : M₂), f c p) (p' : submodule R M₂) :

theorem linear_map.comap_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M₂ →ₗ[R] M) (hf : ∀ (c : M₂), f c p) (p' : submodule R p) :

def linear_map.range {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →ₗ[R] M₂)submodule R M₂

The range of a linear map f : M → M₂ is a submodule of M₂.

Equations
theorem linear_map.range_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

@[simp]
theorem linear_map.mem_range {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {x : M₂} :
x f.range ∃ (y : M), f y = x

theorem linear_map.mem_range_self {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (x : M) :

@[simp]
theorem linear_map.range_id {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

theorem linear_map.range_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :

theorem linear_map.range_comp_le_range {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :

theorem linear_map.range_eq_top {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} :

theorem linear_map.range_le_iff_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M₂} :

theorem linear_map.map_le_range {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} :

theorem linear_map.range_coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :

theorem linear_map.is_compl_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.sup_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

def linear_map.range_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

Restrict the codomain of a linear map f to f.range.

Equations
def linear_map.to_span_singleton (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] :
M → (R →ₗ[R] M)

Given an element x of a module M over R, the natural map from R to scalar multiples of x.

Equations
theorem linear_map.span_singleton_eq_range (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :

The range of to_span_singleton x is the span of x.

theorem linear_map.to_span_singleton_one (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :

def linear_map.ker {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →ₗ[R] M₂)submodule R M

The kernel of a linear map f : M → M₂ is defined to be comap f ⊥. This is equivalent to the set of x : M such that f x = 0. The kernel is a submodule of M.

Equations
@[simp]
theorem linear_map.mem_ker {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {y : M} :
y f.ker f y = 0

@[simp]
theorem linear_map.ker_id {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem linear_map.map_coe_ker {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (x : (f.ker)) :
f x = 0

theorem linear_map.comp_ker_subtype {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :

theorem linear_map.ker_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :

theorem linear_map.ker_le_ker_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
f.ker (g.comp f).ker

theorem linear_map.disjoint_ker {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} :
disjoint p f.ker ∀ (x : M), x pf x = 0x = 0

theorem linear_map.disjoint_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.ker_eq_bot' {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} :
f.ker = ∀ (m : M), f m = 0m = 0

theorem linear_map.le_ker_iff_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {p : submodule R M} :

theorem linear_map.ker_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M₂ →ₗ[R] M) (hf : ∀ (c : M₂), f c p) :

theorem linear_map.range_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (f : M₂ →ₗ[R] M) (hf : ∀ (c : M₂), f c p) :

theorem linear_map.ker_restrict {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p : submodule R M} {f : M →ₗ[R] M} (hf : ∀ (x : M), x pf x p) :

theorem linear_map.map_comap_eq {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (q : submodule R M₂) :

theorem linear_map.map_comap_eq_self {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {q : submodule R M₂} :

@[simp]
theorem linear_map.ker_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem linear_map.range_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem linear_map.ker_eq_top {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} :
f.ker = f = 0

theorem linear_map.range_le_bot_iff {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :
f.range f = 0

theorem linear_map.range_le_ker_iff {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} :
f.range g.ker g.comp f = 0

theorem linear_map.comap_le_comap_iff {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} (hf : f.range = ) {p p' : submodule R M₂} :

theorem linear_map.comap_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} :

theorem linear_map.map_coprod_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : submodule R M) (q : submodule R M₂) :

theorem linear_map.comap_prod_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : submodule R M₂) (q : submodule R M₃) :

theorem linear_map.prod_eq_inf_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (q : submodule R M₂) :

theorem linear_map.prod_eq_sup_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (p : submodule R M) (q : submodule R M₂) :