# mathlib3documentation

algebra.module.equiv

# (Semi)linear equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

• `linear_equiv σ M M₂`, `M ≃ₛₗ[σ] M₂`: an invertible semilinear map. Here, `σ` is a `ring_hom` from `R` to `R₂` and an `e : M ≃ₛₗ[σ] M₂` satisfies `e (c • x) = (σ c) • (e x)`. The plain linear version, with `σ` being `ring_hom.id R`, is denoted by `M ≃ₗ[R] M₂`, and the star-linear version (with `σ` being `star_ring_end`) is denoted by `M ≃ₗ⋆[R] M₂`.

## Implementation notes #

To ensure that composition works smoothly for semilinear equivalences, we use the typeclasses `ring_hom_comp_triple`, `ring_hom_inv_pair` and `ring_hom_surjective` from `algebra/ring/comp_typeclasses`.

The group structure on automorphisms, `linear_equiv.automorphism_group`, is provided elsewhere.

## TODO #

• Parts of this file have not yet been generalized to semilinear maps

## Tags #

linear equiv, linear equivalences, linear isomorphism, linear isomorphic

@[nolint]
structure linear_equiv {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] (σ : R →+* S) {σ' : S →+* R} [ σ'] [ σ] (M : Type u_18) (M₂ : Type u_19) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_18 u_19)

A linear equivalence is an invertible linear map.

Instances for `linear_equiv`
@[nolint]
def linear_equiv.to_add_equiv {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] {M : Type u_18} {M₂ : Type u_19} [add_comm_monoid M₂] [ M] [ M₂] (self : M ≃ₛₗ[σ] M₂) :
M ≃+ M₂
@[nolint]
def linear_equiv.to_linear_map {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] {M : Type u_18} {M₂ : Type u_19} [add_comm_monoid M₂] [ M] [ M₂] (self : M ≃ₛₗ[σ] M₂) :
M →ₛₗ[σ] M₂
@[class]
structure semilinear_equiv_class (F : Type u_16) {R : out_param (Type u_17)} {S : out_param (Type u_18)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ σ'] [ σ] (M : out_param (Type u_19)) (M₂ : out_param (Type u_20)) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_16 u_19 u_20)
• coe : F M M₂
• inv : F M₂ M
• left_inv :
• right_inv :
• coe_injective' : (e g : F),
• map_add : (f : F) (a b : M), f (a + b) = f a + f b
• map_smulₛₗ : (f : F) (r : R) (x : M), f (r x) = σ r f x

`semilinear_equiv_class F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear equivs `M → M₂`.

See also `linear_equiv_class F R M M₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and `f (c • x) = (σ c) • f x`.

Instances of this typeclass
Instances of other typeclasses for `semilinear_equiv_class`
• semilinear_equiv_class.has_sizeof_inst
@[nolint, instance]
def semilinear_equiv_class.to_add_equiv_class (F : Type u_16) {R : out_param (Type u_17)} {S : out_param (Type u_18)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ σ'] [ σ] (M : out_param (Type u_19)) (M₂ : out_param (Type u_20)) [add_comm_monoid M₂] [ M] [ M₂] [self : M₂] :
M₂
@[reducible]
def linear_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (M : out_param (Type u_3)) (M₂ : out_param (Type u_4)) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_1 u_3 u_4)

`linear_equiv_class F R M M₂` asserts `F` is a type of bundled `R`-linear equivs `M → M₂`. This is an abbreviation for `semilinear_equiv_class F (ring_hom.id R) M M₂`.

@[protected, nolint, instance]
def semilinear_equiv_class.semilinear_map_class {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} (F : Type u_16) [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] [s : M₂] :
M M₂
Equations
@[protected, instance]
def linear_equiv.linear_map.has_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
has_coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)
Equations
@[protected, instance]
def linear_equiv.has_coe_to_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
has_coe_to_fun (M ≃ₛₗ[σ] M₂) (λ (_x : M ≃ₛₗ[σ] M₂), M M₂)
Equations
@[simp]
theorem linear_equiv.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] {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 : (r : R) (x : M), to_fun (r x) = σ r to_fun x} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} :
{to_fun := to_fun, map_add' := map_add, map_smul' := map_smul, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv} = to_fun
@[nolint]
def linear_equiv.to_equiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
(M ≃ₛₗ[σ] M₂) M M₂
Equations
theorem linear_equiv.to_equiv_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
@[simp]
theorem linear_equiv.to_equiv_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} :
e₁.to_equiv = e₂.to_equiv e₁ = e₂
theorem linear_equiv.to_linear_map_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
@[simp, norm_cast]
theorem linear_equiv.to_linear_map_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} :
e₁ = e₂ e₁ = e₂
@[protected, instance]
def linear_equiv.semilinear_equiv_class {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
semilinear_equiv_class (M ≃ₛₗ[σ] M₂) σ M M₂
Equations
theorem linear_equiv.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] :
theorem linear_equiv.to_linear_map_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp, norm_cast]
theorem linear_equiv.coe_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.coe_to_equiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.coe_to_linear_map {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.to_fun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[ext]
theorem linear_equiv.ext {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} {e e' : M ≃ₛₗ[σ] M₂} (h : (x : M), e x = e' x) :
e = e'
theorem linear_equiv.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} {e e' : M ≃ₛₗ[σ] M₂} :
e = e' (x : M), e x = e' x
@[protected]
theorem linear_equiv.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} {e : M ≃ₛₗ[σ] M₂} {x x' : M} :
x = x' e x = e x'
@[protected]
theorem linear_equiv.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} {e e' : M ≃ₛₗ[σ] M₂} (h : e = e') (x : M) :
e x = e' x
@[refl]
def linear_equiv.refl (R : Type u_1) (M : Type u_7) [semiring R] [ M] :

The identity map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.refl_apply {R : Type u_1} {M : Type u_7} [semiring R] [ M] (x : M) :
M) x = x
@[symm]
def linear_equiv.symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
M₂ ≃ₛₗ[σ'] M

Linear equivalences are symmetric.

Equations
def linear_equiv.simps.symm_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {σ : R →+* S} {σ' : S →+* R} [ σ'] [ σ] {M : Type u_3} {M₂ : Type u_4} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃ₛₗ[σ] M₂) :
M₂ M
Equations
@[simp]
theorem linear_equiv.inv_fun_eq_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.coe_to_equiv_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[nolint, trans]
def linear_equiv.trans {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₃ σ₁₃] [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₃ : σ₃₂} [ σ₃₁] {re₂₁ : σ₁₂} {re₃₂ : σ₂₃} [ σ₁₃] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
M₁ ≃ₛₗ[σ₁₃] M₃

Linear equivalences are transitive.

Equations
@[simp]
theorem linear_equiv.coe_to_add_equiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
theorem linear_equiv.to_add_monoid_hom_commutes {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :

The two paths coercion can take to an `add_monoid_hom` are equivalent

@[simp]
theorem linear_equiv.trans_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₃ σ₁₃] [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₃ : σ₃₂} [ σ₃₁] {re₂₁ : σ₁₂} {re₃₂ : σ₂₃} [ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₁) :
(e₁₂.trans e₂₃) c = e₂₃ (e₁₂ c)
theorem linear_equiv.coe_trans {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₃ σ₁₃] [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₃ : σ₃₂} [ σ₃₁] {re₂₁ : σ₁₂} {re₃₂ : σ₂₃} [ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
(e₁₂.trans e₂₃) = e₂₃.comp e₁₂
@[simp]
theorem linear_equiv.apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (c : M₂) :
e ((e.symm) c) = c
@[simp]
theorem linear_equiv.symm_apply_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (b : M) :
(e.symm) (e b) = b
@[simp]
theorem linear_equiv.trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₃ σ₁₃] [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₃ : σ₃₂} [ σ₃₁] {re₂₁ : σ₁₂} {re₃₂ : σ₂₃} [ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
(e₁₂.trans e₂₃).symm = e₂₃.symm.trans e₁₂.symm
theorem linear_equiv.symm_trans_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₃ σ₁₃] [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₃ : σ₃₂} [ σ₃₁] {re₂₁ : σ₁₂} {re₃₂ : σ₂₃} [ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₃) :
((e₁₂.trans e₂₃).symm) c = (e₁₂.symm) ((e₂₃.symm) c)
@[simp]
theorem linear_equiv.trans_refl {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
e.trans M₂) = e
@[simp]
theorem linear_equiv.refl_trans {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
M).trans e = e
theorem linear_equiv.symm_apply_eq {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} :
(e.symm) x = y x = e y
theorem linear_equiv.eq_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} :
y = (e.symm) x e y = x
theorem linear_equiv.eq_comp_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : M₂ α) (g : M₁ α) :
f = g (e₁₂.symm) f e₁₂ = g
theorem linear_equiv.comp_symm_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : M₂ α) (g : M₁ α) :
g (e₁₂.symm) = f g = f e₁₂
theorem linear_equiv.eq_symm_comp {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : α M₁) (g : α M₂) :
f = (e₁₂.symm) g e₁₂ f = g
theorem linear_equiv.symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : α M₁) (g : α M₂) :
(e₁₂.symm) g = f g = e₁₂ f
theorem linear_equiv.eq_comp_to_linear_map_symm {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} [ σ₂₃ σ₁₃] {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
f = g.comp e₁₂.symm.to_linear_map f.comp e₁₂.to_linear_map = g
theorem linear_equiv.comp_to_linear_map_symm_eq {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} [ σ₂₃ σ₁₃] {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
g.comp e₁₂.symm.to_linear_map = f g = f.comp e₁₂.to_linear_map
theorem linear_equiv.eq_to_linear_map_symm_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
f = e₁₂.symm.to_linear_map.comp g e₁₂.to_linear_map.comp f = g
theorem linear_equiv.to_linear_map_symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R₁] [semiring R₂] [semiring R₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ σ₂₁ σ₃₁] {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
e₁₂.symm.to_linear_map.comp g = f g = e₁₂.to_linear_map.comp f
@[simp]
theorem linear_equiv.refl_symm {R : Type u_1} {M : Type u_7} [semiring R] [ M] :
M).symm =
@[simp]
theorem linear_equiv.self_trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
f.trans f.symm = M₁
@[simp]
theorem linear_equiv.symm_trans_self {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
f.symm.trans f = M₂
@[simp, norm_cast]
theorem linear_equiv.refl_to_linear_map {R : Type u_1} {M : Type u_7} [semiring R] [ M] :
@[simp, norm_cast]
theorem linear_equiv.comp_coe {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
f'.comp f = (f.trans f')
@[simp]
theorem linear_equiv.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (h₁ : (x y : M), e (x + y) = e x + e y) (h₂ : (r : R) (x : M), e (r x) = σ r e x) (f : M₂ M) (h₃ : e) (h₄ : e) :
{to_fun := e, map_add' := h₁, map_smul' := h₂, inv_fun := f, left_inv := h₃, right_inv := h₄} = e
@[protected]
theorem linear_equiv.map_add {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (a b : M) :
e (a + b) = e a + e b
@[protected]
theorem linear_equiv.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
e 0 = 0
@[protected, simp]
theorem linear_equiv.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (c : R) (x : M) :
e (c x) = σ c e x
theorem linear_equiv.map_smul {R₁ : Type u_2} {N₁ : Type u_11} {N₂ : Type u_12} [semiring R₁] [add_comm_monoid N₁] [add_comm_monoid N₂] {module_N₁ : module R₁ N₁} {module_N₂ : module R₁ N₂} (e : N₁ ≃ₗ[R₁] N₂) (c : R₁) (x : N₁) :
e (c x) = c e x
@[simp]
theorem linear_equiv.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) {x : M} :
e x = 0 x = 0
theorem linear_equiv.map_ne_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) {x : M} :
e x 0 x 0
@[simp]
theorem linear_equiv.symm_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
e.symm.symm = e
theorem linear_equiv.symm_bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {σ : R →+* S} {σ' : S →+* R} [ M] [ M₂] [ σ] [ σ'] :
@[simp]
theorem linear_equiv.mk_coe' {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ M) (h₁ : (x y : M₂), f (x + y) = f x + f y) (h₂ : (r : S) (x : M₂), f (r x) = σ' r f x) (h₃ : f) (h₄ : f) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, inv_fun := e, left_inv := h₃, right_inv := h₄} = e.symm
@[simp]
theorem linear_equiv.symm_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ M) (h₁ : (x y : M), e (x + y) = e x + e y) (h₂ : (r : R) (x : M), e (r x) = σ r e x) (h₃ : e) (h₄ : e) :
{to_fun := e, map_add' := h₁, map_smul' := h₂, inv_fun := f, left_inv := h₃, right_inv := h₄}.symm = {to_fun := f, map_add' := _, map_smul' := _, inv_fun := e, left_inv := _, right_inv := _}
@[simp]
theorem linear_equiv.coe_symm_mk {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M₂] [ M] [ 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 : (r : R) (x : M), to_fun (r x) = (ring_hom.id R) r to_fun x} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} :
({to_fun := to_fun, map_add' := map_add, map_smul' := map_smul, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv}.symm) = inv_fun
@[protected]
theorem linear_equiv.bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[protected]
theorem linear_equiv.injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[protected]
theorem linear_equiv.surjective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) :
@[protected]
theorem linear_equiv.image_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (s : set M) :
e '' s = (e.symm) ⁻¹' s
@[protected]
theorem linear_equiv.image_symm_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] {module_M : M} {module_S_M₂ : M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : σ'} {re₂ : σ} (e : M ≃ₛₗ[σ] M₂) (s : set M₂) :
(e.symm) '' s = e ⁻¹' s
@[simp]
theorem ring_equiv.to_semilinear_equiv_apply {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R ≃+* S) (ᾰ : R) :
def ring_equiv.to_semilinear_equiv {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R ≃+* S) :

Interpret a `ring_equiv` `f` as an `f`-semilinear equiv.

Equations
@[simp]
theorem ring_equiv.to_semilinear_equiv_symm_apply {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R ≃+* S) (ᾰ : S) :
def linear_equiv.of_involutive {R : Type u_1} {M : Type u_7} [semiring R] {σ σ' : R →+* R} [ σ'] [ σ] {module_M : M} (f : M →ₛₗ[σ] M) (hf : function.involutive f) :

An involutive linear map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.coe_of_involutive {R : Type u_1} {M : Type u_7} [semiring R] {σ σ' : R →+* R} [ σ'] [ σ] {module_M : M} (f : M →ₛₗ[σ] M) (hf : function.involutive f) :
def linear_equiv.restrict_scalars (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (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 equivalence from `M` to `M₂` is also an `R`-linear equivalence.

See also `linear_map.restrict_scalars`.

Equations
@[simp]
theorem linear_equiv.restrict_scalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (f : M ≃ₗ[S] M₂) (ᾰ : M) :
= f ᾰ
@[simp]
theorem linear_equiv.restrict_scalars_symm_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (f : M ≃ₗ[S] M₂) (ᾰ : M₂) :
.symm) = (f.symm) ᾰ
theorem linear_equiv.restrict_scalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] :
@[simp]
theorem linear_equiv.restrict_scalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (f g : M ≃ₗ[S] M₂) :
@[protected, instance]
def linear_equiv.automorphism_group {R : Type u_1} {M : Type u_7} [semiring R] [ M] :
Equations
• linear_equiv.automorphism_group = {mul := λ (f g : M ≃ₗ[R] M), g.trans f, mul_assoc := _, one := _inst_9, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default M) (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_6 linear_equiv.automorphism_group._proof_7, npow_zero' := _, npow_succ' := _, inv := λ (f : M ≃ₗ[R] M), f.symm, div := div_inv_monoid.div._default (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_10 M) linear_equiv.automorphism_group._proof_11 linear_equiv.automorphism_group._proof_12 (div_inv_monoid.npow._default M) (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_6 linear_equiv.automorphism_group._proof_7) linear_equiv.automorphism_group._proof_13 linear_equiv.automorphism_group._proof_14 (λ (f : M ≃ₗ[R] M), f.symm), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_16 M) linear_equiv.automorphism_group._proof_17 linear_equiv.automorphism_group._proof_18 (div_inv_monoid.npow._default M) (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_6 linear_equiv.automorphism_group._proof_7) linear_equiv.automorphism_group._proof_19 linear_equiv.automorphism_group._proof_20 (λ (f : M ≃ₗ[R] M), f.symm), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem linear_equiv.automorphism_group.to_linear_map_monoid_hom_apply {R : Type u_1} {M : Type u_7} [semiring R] [ M] (ᾰ : M ≃ₗ[R] M) :

Restriction from `R`-linear automorphisms of `M` to `R`-linear endomorphisms of `M`, promoted to a monoid hom.

Equations
@[protected, instance]

The tautological action by `M ≃ₗ[R] M` on `M`.

This generalizes `function.End.apply_mul_action`.

Equations
@[protected, simp]
theorem linear_equiv.smul_def {R : Type u_1} {M : Type u_7} [semiring R] [ M] (f : M ≃ₗ[R] M) (a : M) :
f a = f a
@[protected, instance]
def linear_equiv.apply_has_faithful_smul {R : Type u_1} {M : Type u_7} [semiring R] [ M] :

`linear_equiv.apply_distrib_mul_action` is faithful.

@[protected, instance]
def linear_equiv.apply_smul_comm_class {R : Type u_1} {M : Type u_7} [semiring R] [ M] :
(M ≃ₗ[R] M) M
@[protected, instance]
def linear_equiv.apply_smul_comm_class' {R : Type u_1} {M : Type u_7} [semiring R] [ M] :
@[simp]
theorem linear_equiv.of_subsingleton_symm_apply {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] [subsingleton M] [subsingleton M₂] (_x : M₂) :
M₂).symm) _x = 0
def linear_equiv.of_subsingleton {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] [subsingleton M] [subsingleton M₂] :
M ≃ₗ[R] M₂

Any two modules that are subsingletons are isomorphic.

Equations
@[simp]
theorem linear_equiv.of_subsingleton_apply {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] [subsingleton M] [subsingleton M₂] (_x : M) :
_x = 0
@[simp]
theorem linear_equiv.of_subsingleton_self {R : Type u_1} (M : Type u_7) [semiring R] [ M] [subsingleton M] :
@[simp]
theorem module.comp_hom.to_linear_equiv_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R ≃+* S) (ᾰ : R) :
= g ᾰ
def module.comp_hom.to_linear_equiv {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R ≃+* S) :

`g : R ≃+* S` is `R`-linear when the module structure on `S` is `module.comp_hom S g` .

Equations
@[simp]
theorem module.comp_hom.to_linear_equiv_symm_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R ≃+* S) (ᾰ : S) :
= (g.symm) ᾰ
@[simp]
theorem distrib_mul_action.to_linear_equiv_symm_apply (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [ M] [group S] [ M] [ M] (s : S) (ᾰ : M) :
.symm) =
def distrib_mul_action.to_linear_equiv (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [ M] [group S] [ M] [ M] (s : S) :

Each element of the group defines a linear equivalence.

This is a stronger version of `distrib_mul_action.to_add_equiv`.

Equations
@[simp]
theorem distrib_mul_action.to_linear_equiv_apply (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [ M] [group S] [ M] [ M] (s : S) (ᾰ : M) :
=
def distrib_mul_action.to_module_aut (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [ M] [group S] [ M] [ M] :
S →* M ≃ₗ[R] M

Each element of the group defines a module automorphism.

This is a stronger version of `distrib_mul_action.to_add_aut`.

Equations
@[simp]
theorem distrib_mul_action.to_module_aut_apply (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [ M] [group S] [ M] [ M] (s : S) :
def add_equiv.to_linear_equiv {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃+ M₂) (h : (c : R) (x : M), e (c x) = c e x) :
M ≃ₗ[R] M₂

An additive equivalence whose underlying function preserves `smul` is a linear equivalence.

Equations
@[simp]
theorem add_equiv.coe_to_linear_equiv {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃+ M₂) (h : (c : R) (x : M), e (c x) = c e x) :
@[simp]
theorem add_equiv.coe_to_linear_equiv_symm {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃+ M₂) (h : (c : R) (x : M), e (c x) = c e x) :
def add_equiv.to_nat_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M₂] (e : M ≃+ M₂) :

An additive equivalence between commutative additive monoids is a linear equivalence between ℕ-modules

Equations
@[simp]
theorem add_equiv.coe_to_nat_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M₂] (e : M ≃+ M₂) :
@[simp]
theorem add_equiv.to_nat_linear_equiv_to_add_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M₂] (e : M ≃+ M₂) :
@[simp]
theorem linear_equiv.to_add_equiv_to_nat_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M₂] (e : M ≃ₗ[] M₂) :
@[simp]
theorem add_equiv.to_nat_linear_equiv_symm {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M₂] (e : M ≃+ M₂) :
@[simp]
@[simp]
theorem add_equiv.to_nat_linear_equiv_trans {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [add_comm_monoid M₂] [add_comm_monoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
def add_equiv.to_int_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_group M₂] (e : M ≃+ M₂) :

An additive equivalence between commutative additive groups is a linear equivalence between ℤ-modules

Equations
@[simp]
theorem add_equiv.coe_to_int_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_group M₂] (e : M ≃+ M₂) :
@[simp]
theorem add_equiv.to_int_linear_equiv_to_add_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_group M₂] (e : M ≃+ M₂) :
@[simp]
theorem linear_equiv.to_add_equiv_to_int_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_group M₂] (e : M ≃ₗ[] M₂) :
@[simp]
theorem add_equiv.to_int_linear_equiv_symm {M : Type u_7} {M₂ : Type u_9} [add_comm_group M₂] (e : M ≃+ M₂) :
@[simp]
@[simp]
theorem add_equiv.to_int_linear_equiv_trans {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [add_comm_group M₂] [add_comm_group M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :