mathlib documentation

algebra.module.linear_map

Linear maps and linear equivalences

In this file we define

Tags

linear map, linear equiv, linear equivalences, linear isomorphism, linear isomorphic

structure is_linear_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 → M₂) :
Prop
  • map_add : ∀ (x y : M), f (x + y) = f x + f y
  • map_smul : ∀ (c : R) (x : M), f (c x) = c f x

A map f between semimodules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. The predicate is_linear_map R f asserts this property. A bundled version is available with linear_map, and should be favored over is_linear_map most of the time.

structure linear_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₂] :
Type (max v w)

A map f between semimodules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. Elements of linear_map R M M₂ (available under the notation M →ₗ[R] M₂) are bundled versions of such maps. An unbundled version is available with the predicate is_linear_map, but it should be avoided most of the time.

def linear_map.to_add_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₂] (s : M →ₗ[R] M₂) :
add_hom M M₂

The add_hom underlying a linear_map.

def linear_map.to_mul_action_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₂] (s : M →ₗ[R] M₂) :
M →[R] M₂

The mul_action_hom underlying a linear_map.

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

Equations
@[simp]
theorem linear_map.coe_mk {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M → M₂) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : M), f (m x) = m f x) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f

def linear_map.id {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] :

Identity map as a linear_map

Equations
theorem linear_map.id_apply {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :

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

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

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

theorem linear_map.coe_injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
function.injective (λ (f : M →ₗ[R] M₂), show M → M₂, from f)

@[ext]
theorem linear_map.ext {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f g : M →ₗ[R] M₂} (H : ∀ (x : M), f x = g x) :
f = g

theorem linear_map.congr_arg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →ₗ[R] M₂} {x x' : M} :
x = x'f x = f x'

theorem linear_map.congr_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f g : M →ₗ[R] M₂} (h : f = g) (x : M) :
f x = g x

If two linear maps are equal, they are equal at each point.

theorem linear_map.ext_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f g : M →ₗ[R] M₂} :
f = g ∀ (x : M), f x = g x

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

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

@[simp]
theorem linear_map.map_smul_of_tower {M : Type w} {M₂ : Type x} [add_comm_monoid M] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [has_scalar R S] [has_scalar R M] [semimodule S M] [is_scalar_tower R S M] [has_scalar R M₂] [semimodule S M₂] [is_scalar_tower R S M₂] (f : M →ₗ[S] M₂) (c : R) (x : M) :
f (c x) = c f x

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

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

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

convert a linear map to an additive map

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

def linear_map.restrict_scalars (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {S : Type u_1} [has_scalar R S] [semiring S] [semimodule S M] [semimodule S M₂] [is_scalar_tower R S M] [is_scalar_tower R S M₂] (f : M →ₗ[S] M₂) :
M →ₗ[R] M₂

If M and M₂ are both R-semimodules and S-semimodules and R-semimodule structures are defined by an action of R on S (formally, we have two scalar towers), then any S-linear map from M to M₂ is R-linear.

See also linear_map.map_smul_of_tower.

Equations
@[simp]
theorem linear_map.map_sum {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) {ι : Type u_1} {t : finset ι} {g : ι → M} :
f (∑ (i : ι) in t, g i) = ∑ (i : ι) in t, f (g i)

@[ext]
theorem linear_map.ext_ring {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] {f g : R →ₗ[R] M} (h : f 1 = g 1) :
f = g

If two R-linear maps from R are equal on 1, then they are equal.

def linear_map.comp {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
M →ₗ[R] M₃

Composition of two linear maps is a linear map

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

theorem linear_map.comp_coe {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
f g = (f.comp g)

def linear_map.inverse {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (g : M₂ → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
M₂ →ₗ[R] M

If a function g is a left and right inverse of a linear map f, then g is linear itself.

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

@[simp]
theorem linear_map.map_sub {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) (x y : M) :
f (x - y) = f x - f y

@[instance]
def linear_map.is_add_group_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :

def is_linear_map.mk' {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M → M₂) (H : is_linear_map R f) :
M →ₗ[R] M₂

Convert an is_linear_map predicate to a linear_map

Equations
@[simp]
theorem is_linear_map.mk'_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M → M₂} (H : is_linear_map R f) (x : M) :

theorem is_linear_map.is_linear_map_smul {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [semimodule R M] (c : R) :
is_linear_map R (λ (z : M), c z)

theorem is_linear_map.is_linear_map_smul' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (a : M) :
is_linear_map R (λ (c : R), c a)

theorem is_linear_map.map_zero {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M → M₂} (lin : is_linear_map R f) :
f 0 = 0

theorem is_linear_map.is_linear_map_neg {R : Type u} {M : Type w} [semiring R] [add_comm_group M] [semimodule R M] :
is_linear_map R (λ (z : M), -z)

theorem is_linear_map.map_neg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] {f : M → M₂} (lin : is_linear_map R f) (x : M) :
f (-x) = -f x

theorem is_linear_map.map_sub {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] {f : M → M₂} (lin : is_linear_map R f) (x y : M) :
f (x - y) = f x - f y

def module.End (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] :
Type v

Linear endomorphisms of a module, with associated ring structure linear_map.endomorphism_semiring and algebra structure module.endomorphism_algebra.

def add_monoid_hom.to_int_linear_map {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a -linear map.

Equations
def add_monoid_hom.to_rat_linear_map {M : Type w} {M₂ : Type x} [add_comm_group M] [vector_space M] [add_comm_group M₂] [vector_space M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a -linear map.

Equations

Linear equivalences

@[nolint]
structure linear_equiv (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 (max v w)

A linear equivalence is an invertible linear map.

@[nolint]
def linear_equiv.to_add_equiv {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 : M ≃ₗ[R] M₂) :
M ≃+ M₂

@[nolint]
def linear_equiv.to_linear_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₂] (s : M ≃ₗ[R] M₂) :
M →ₗ[R] M₂

@[instance]
def linear_equiv.linear_map.has_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_coe (M ≃ₗ[R] M₂) (M →ₗ[R] M₂)

Equations
@[instance]
def linear_equiv.has_coe_to_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

Equations
@[simp]
theorem linear_equiv.mk_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {to_fun : M → M₂} {inv_fun : M₂ → M} {map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y} {map_smul : ∀ (m : R) (x : M), to_fun (m x) = m to_fun x} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} {a : M} :
{to_fun := to_fun, map_add' := map_add, map_smul' := map_smul, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv} a = to_fun a

@[nolint]
def linear_equiv.to_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M ≃ₗ[R] M₂)M M₂

Equations
theorem linear_equiv.injective_to_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem linear_equiv.to_equiv_inj {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {e₁ e₂ : M ≃ₗ[R] M₂} :
e₁.to_equiv = e₂.to_equiv e₁ = e₂

theorem linear_equiv.injective_to_linear_map {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem linear_equiv.to_linear_map_inj {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {e₁ e₂ : M ≃ₗ[R] M₂} :
e₁ = e₂ e₁ = e₂

@[simp]
theorem linear_equiv.coe_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

@[simp]
theorem linear_equiv.coe_to_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

@[simp]
theorem linear_equiv.to_fun_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {m : M} :
e.to_fun m = e m

@[ext]
theorem linear_equiv.ext {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {e e' : M ≃ₗ[R] M₂} (h : ∀ (x : M), e x = e' x) :
e = e'

def linear_equiv.refl (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [semimodule R M] :

The identity map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.refl_apply {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :

def linear_equiv.symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :
M₂ ≃ₗ[R] M

Linear equivalences are symmetric.

Equations
def linear_equiv.simps.inv_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃ₗ[R] M₂) :
M₂ → M

See Note [custom simps projection]

Equations
@[simp]
theorem linear_equiv.inv_fun_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {m : M₂} :
e.inv_fun m = (e.symm) m

def linear_equiv.trans {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :
M ≃ₗ[R] M₃

Linear equivalences are transitive.

Equations
@[simp]
theorem linear_equiv.coe_to_add_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

@[simp]
theorem linear_equiv.trans_apply {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) (c : M) :
(e₁.trans e₂) c = e₂ (e₁ c)

@[simp]
theorem linear_equiv.apply_symm_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) (c : M₂) :
e ((e.symm) c) = c

@[simp]
theorem linear_equiv.symm_apply_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) (b : M) :
(e.symm) (e b) = b

@[simp]
theorem linear_equiv.symm_trans_apply {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) (c : M₃) :
((e₁.trans e₂).symm) c = (e₁.symm) ((e₂.symm) c)

@[simp]
theorem linear_equiv.trans_refl {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

@[simp]
theorem linear_equiv.refl_trans {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

theorem linear_equiv.symm_apply_eq {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {x : M₂} {y : M} :
(e.symm) x = y x = e y

theorem linear_equiv.eq_symm_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {x : M₂} {y : M} :
y = (e.symm) x e y = x

@[simp]
theorem linear_equiv.trans_symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M ≃ₗ[R] M₂) :

@[simp]
theorem linear_equiv.symm_trans {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M ≃ₗ[R] M₂) :

@[simp]

@[simp]
theorem linear_equiv.comp_coe {R : Type u} {M : Type w} {M₂ : Type x} {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' : M₂ ≃ₗ[R] M₃) :
f'.comp f = (f.trans f')

@[simp]
theorem linear_equiv.map_add {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) (a b : M) :
e (a + b) = e a + e b

@[simp]
theorem linear_equiv.map_zero {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :
e 0 = 0

@[simp]
theorem linear_equiv.map_smul {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) (c : R) (x : M) :
e (c x) = c e x

@[simp]
theorem linear_equiv.map_sum {R : Type u} {M : Type w} {M₂ : Type x} {ι : Type z} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {s : finset ι} (u : ι → M) :
e (∑ (i : ι) in s, u i) = ∑ (i : ι) in s, e (u i)

@[simp]
theorem linear_equiv.map_eq_zero_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {x : M} :
e x = 0 x = 0

theorem linear_equiv.map_ne_zero_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) {x : M} :
e x 0 x 0

@[simp]
theorem linear_equiv.symm_symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :
e.symm.symm = e

theorem linear_equiv.bijective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

theorem linear_equiv.injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

theorem linear_equiv.surjective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) :

theorem linear_equiv.image_eq_preimage {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (e : M ≃ₗ[R] M₂) (s : set M) :
e '' s = (e.symm) ⁻¹' s

def linear_equiv.of_involutive {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) (hf : function.involutive f) :

An involutive linear map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.coe_of_involutive {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) (hf : function.involutive f) :