(Semi)linear equivalences

In this file we define

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

Implementation notes

To ensure that composition works smoothly for semilinear equivalences, we use the typeclasses RingHomCompTriple, RingHomInvPair and RingHomSurjective from Algebra/Ring/CompTypeclasses.

The group structure on automorphisms, LinearEquiv.automorphismGroup, 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

structure LinearEquiv {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂, M ≃+ M₂ : Type (max u_16 u_17)

A linear equivalence is an invertible linear map.

• toFun : M → M₂
• map_add' (x y : M) : (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
• map_smul' (m : R) (x : M) : (↑self).toFun (m • x) = σ m • (↑self).toFun x
• invFun : M₂ → M
• left_inv : Function.LeftInverse self.invFun (↑self).toFun
• right_inv : Function.RightInverse self.invFun (↑self).toFun

def «term_≃ₛₗ[_]_» : Lean.TrailingParserDescr

M ≃ₛₗ[σ] M₂ denotes the type of linear equivalences between M and M₂ over a ring homomorphism σ.

def «term_≃ₗ[_]_» : Lean.TrailingParserDescr

M ≃ₗ[R] M₂ denotes the type of linear equivalences between M and M₂ over a plain linear map M →ₗ M₂.

class SemilinearEquivClass (F : Type u_14) {R : outParam (Type u_15)} {S : outParam (Type u_16)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) {σ' : outParam (S →+* R)} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : outParam (Type u_17)) (M₂ : outParam (Type u_18)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] [EquivLike F M M₂] extends AddEquivClass F M M₂ : Prop

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

See also LinearEquivClass 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.

• 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

  Applying a semilinear equivalence f over σ to r • x equals σ r • f x.

@[reducible, inline]

abbrev LinearEquivClass (F : Type u_14) (R : outParam (Type u_15)) (M : outParam (Type u_16)) (M₂ : outParam (Type u_17)) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [EquivLike F M M₂] : Prop

LinearEquivClass F R M M₂ asserts F is a type of bundled R-linear equivs M → M₂. This is an abbreviation for SemilinearEquivClass F (RingHom.id R) M M₂.

@[instance 100]

instance SemilinearEquivClass.instSemilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} (F : Type u_14) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [s : SemilinearEquivClass F σ M M₂] : SemilinearMapClass F σ M M₂

def SemilinearEquivClass.semilinearEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} {F : Type u_14} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] (f : F) : M ≃ₛₗ[σ] M₂

Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence.

@[implicit_reducible]

instance SemilinearEquivClass.instCoeToSemilinearEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} {F : Type u_14} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] : CoeHead F (M ≃ₛₗ[σ] M₂)

Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence.

@[implicit_reducible]

instance LinearEquiv.instCoeLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)

def LinearEquiv.toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] M₂) : M ≃ M₂

The equivalence of types underlying a linear equivalence.

theorem LinearEquiv.toEquiv_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Function.Injective toEquiv

@[simp]

theorem LinearEquiv.toEquiv_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

theorem LinearEquiv.toLinearMap_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Function.Injective toLinearMap

@[simp]

theorem LinearEquiv.toLinearMap_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} : ↑e₁ = ↑e₂ ↔ e₁ = e₂

@[implicit_reducible]

instance LinearEquiv.instEquivLike {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : EquivLike (M ≃ₛₗ[σ] M₂) M M₂

instance LinearEquiv.instSemilinearEquivClass {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂

theorem LinearEquiv.toLinearMap_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {e : M ≃ₛₗ[σ] M₂} : ↑e = ↑e

@[simp]

theorem LinearEquiv.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {f : M →ₛₗ[σ] M₂} {invFun : M₂ → M} {left_inv : Function.LeftInverse invFun f.toFun} {right_inv : Function.RightInverse invFun f.toFun} : ⇑{ toLinearMap := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv } = ⇑f

theorem LinearEquiv.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Function.Injective DFunLike.coe

@[simp]

theorem SemilinearEquivClass.semilinearEquiv_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {F : Type u_14} [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] (f : F) (x : M) : ↑f x = f x

@[simp]

theorem LinearEquiv.coe_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑↑e = ⇑e

@[simp]

theorem LinearEquiv.coe_toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑e.toEquiv = ⇑e

@[simp]

theorem LinearEquiv.coe_toLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑↑e = ⇑e

theorem LinearEquiv.toFun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : (↑e).toFun = ⇑e

theorem LinearEquiv.ext {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂} (h : ∀ (x : M), e x = e' x) : e = e'

theorem LinearEquiv.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂} : e = e' ↔ ∀ (x : M), e x = e' x

theorem LinearEquiv.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e : M ≃ₛₗ[σ] M₂} {x x' : M} : x = x' → e x = e x'

theorem LinearEquiv.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂} (h : e = e') (x : M) : e x = e' x

def LinearEquiv.refl (R : Type u_1) (M : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] : M ≃ₗ[R] M

The identity map is a linear equivalence.

@[simp]

theorem LinearEquiv.refl_apply {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : (refl R M) x = x

def LinearEquiv.symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : M₂ ≃ₛₗ[σ'] M

Linear equivalences are symmetric.

def LinearEquiv.Simps.apply {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (e : M ≃ₛₗ[σ] M₂) : M → M₂

See Note [custom simps projection]

def LinearEquiv.Simps.symm_apply {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (e : M ≃ₛₗ[σ] M₂) : M₂ → M

See Note [custom simps projection]

@[simp]

theorem LinearEquiv.invFun_eq_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.invFun = ⇑e.symm

theorem LinearEquiv.coe_toEquiv_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.toEquiv.symm = ↑e.symm

@[simp]

theorem LinearEquiv.toEquiv_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.symm.toEquiv = e.toEquiv.symm

@[simp]

theorem LinearEquiv.coe_symm_toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑e.toEquiv.symm = ⇑e.symm

def LinearEquiv.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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) : M₁ ≃ₛₗ[σ₁₃] M₃

Linear equivalences are transitive.

def LinearEquiv.transNotation : Lean.TrailingParserDescr

e₁ ≪≫ₗ e₂ denotes the composition of the linear equivalences e₁ and e₂.

def LinearEquiv.symmEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} : (M ≃ₛₗ[σ] M₂) ≃ M₂ ≃ₛₗ[σ'] M

LinearEquiv.symm defines an equivalence between α ≃ₛₗ[σ] β and β ≃ₛₗ[σ] α.

@[simp]

theorem LinearEquiv.symmEquiv_symm_apply_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M₂ ≃ₛₗ[σ'] M) (a : M) : (symmEquiv.symm e) a = ((↑e).inverse ⇑e.symm ⋯ ⋯) a

@[simp]

theorem LinearEquiv.symmEquiv_apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a✝ : M) : (symmEquiv e).symm a✝ = e a✝

@[simp]

theorem LinearEquiv.symmEquiv_symm_apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M₂ ≃ₛₗ[σ'] M) (a✝ : M₂) : (symmEquiv.symm e).symm a✝ = e a✝

@[simp]

theorem LinearEquiv.symmEquiv_apply_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a : M₂) : (symmEquiv e) a = ((↑e).inverse ⇑e.symm ⋯ ⋯) a

theorem LinearEquiv.coe_toAddEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.toAddEquiv = ↑e

@[simp]

theorem LinearEquiv.coe_addEquiv_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (x : M) : ↑e x = e x

theorem LinearEquiv.toAddMonoidHom_commutes {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : (↑e).toAddMonoidHom = e.toAddEquiv.toAddMonoidHom

The two paths coercion can take to an AddMonoidHom are equivalent

theorem LinearEquiv.coe_toAddEquiv_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} : ↑e₁₂.symm = (↑e₁₂).symm

@[simp]

theorem LinearEquiv.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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₁) : (e₁₂.trans e₂₃) c = e₂₃ (e₁₂ c)

theorem LinearEquiv.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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} : ↑(e₁₂.trans e₂₃) = ↑e₂₃ ∘ₛₗ ↑e₁₂

@[simp]

theorem LinearEquiv.apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : M₂) : e (e.symm c) = c

@[simp]

theorem LinearEquiv.symm_apply_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (b : M) : e.symm (e b) = b

theorem LinearEquiv.comp_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ↑e ∘ₛₗ ↑e.symm = LinearMap.id

theorem LinearEquiv.symm_comp {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ↑e.symm ∘ₛₗ ↑e = LinearMap.id

@[simp]

theorem LinearEquiv.comp_symm_assoc {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} (f : M₃ →ₛₗ[σ₃₂] M₂) [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] : ↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f = f

@[simp]

theorem LinearEquiv.symm_comp_assoc {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} (f : M₃ →ₛₗ[σ₃₁] M₁) [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] : ↑e₁₂.symm ∘ₛₗ ↑e₁₂ ∘ₛₗ f = f

@[simp]

theorem LinearEquiv.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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} : (e₁₂.trans e₂₃).symm = e₂₃.symm.trans e₁₂.symm

theorem LinearEquiv.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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₃) : (e₁₂.trans e₂₃).symm c = e₁₂.symm (e₂₃.symm c)

@[simp]

theorem LinearEquiv.trans_refl {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.trans (refl S M₂) = e

@[simp]

theorem LinearEquiv.refl_trans {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : (refl R M).trans e = e

theorem LinearEquiv.symm_apply_eq {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} : e.symm x = y ↔ x = e y

theorem LinearEquiv.eq_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} : y = e.symm x ↔ e y = x

theorem LinearEquiv.eq_comp_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : M₂ → α) (g : M₁ → α) : f = g ∘ ⇑e₁₂.symm ↔ f ∘ ⇑e₁₂ = g

theorem LinearEquiv.comp_symm_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : M₂ → α) (g : M₁ → α) : g ∘ ⇑e₁₂.symm = f ↔ g = f ∘ ⇑e₁₂

theorem LinearEquiv.eq_symm_comp {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : α → M₁) (g : α → M₂) : f = ⇑e₁₂.symm ∘ g ↔ ⇑e₁₂ ∘ f = g

theorem LinearEquiv.symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : α → M₁) (g : α → M₂) : ⇑e₁₂.symm ∘ g = f ↔ g = ⇑e₁₂ ∘ f

@[simp]

theorem LinearEquiv.comp_coe {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f : M₁ ≃ₛₗ[σ₁₂] M₂) (f' : M₂ ≃ₛₗ[σ₂₃] M₃) : ↑f' ∘ₛₗ ↑f = ↑(f.trans f')

theorem LinearEquiv.trans_assoc {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} {M₄ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {module_M₄ : Module R₄ M₄} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₁₄ : R₁ →+* R₄} {σ₄₁ : R₄ →+* R₁} [RingHomInvPair σ₁₄ σ₄₁] [RingHomInvPair σ₄₁ σ₁₄] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₂₄ : R₂ →+* R₄} {σ₄₂ : R₄ →+* R₂} [RingHomInvPair σ₂₄ σ₄₂] [RingHomInvPair σ₄₂ σ₂₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomCompTriple σ₄₂ σ₂₁ σ₄₁] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₄₃ σ₃₁ σ₄₁] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₄₃ σ₃₂ σ₄₂] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) (e₃₄ : M₃ ≃ₛₗ[σ₃₄] M₄) : (e₁₂.trans e₂₃).trans e₃₄ = e₁₂.trans (e₂₃.trans e₃₄)

theorem LinearEquiv.eq_comp_toLinearMap_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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) : f = g ∘ₛₗ ↑e₁₂.symm ↔ f ∘ₛₗ ↑e₁₂ = g

theorem LinearEquiv.comp_toLinearMap_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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) : g ∘ₛₗ ↑e₁₂.symm = f ↔ g = f ∘ₛₗ ↑e₁₂

theorem LinearEquiv.eq_toLinearMap_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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) : f = ↑e₁₂.symm ∘ₛₗ g ↔ ↑e₁₂ ∘ₛₗ f = g

theorem LinearEquiv.toLinearMap_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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) : ↑e₁₂.symm ∘ₛₗ g = f ↔ g = ↑e₁₂ ∘ₛₗ f

@[simp]

theorem LinearEquiv.comp_toLinearMap_eq_iff {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f g : M₃ →ₛₗ[σ₃₁] M₁) : ↑e₁₂ ∘ₛₗ f = ↑e₁₂ ∘ₛₗ g ↔ f = g

@[simp]

theorem LinearEquiv.eq_comp_toLinearMap_iff {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f g : M₂ →ₛₗ[σ₂₃] M₃) : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂ ↔ f = g

theorem LinearEquiv.comp_symm_cancel_left {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ →ₛₗ[σ₃₂] M₂) : ↑e ∘ₛₗ ↑e.symm ∘ₛₗ f = f

theorem LinearEquiv.symm_comp_cancel_left {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ →ₛₗ[σ₃₁] M₁) : ↑e.symm ∘ₛₗ ↑e ∘ₛₗ f = f

theorem LinearEquiv.comp_symm_cancel_right {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₂ →ₛₗ[σ₂₃] M₃) : (f ∘ₛₗ ↑e) ∘ₛₗ ↑e.symm = f

theorem LinearEquiv.symm_comp_cancel_right {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid 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₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₁ →ₛₗ[σ₁₃] M₃) : (f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e = f

theorem LinearEquiv.trans_symm_cancel_left {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₁ ≃ₛₗ[σ₁₃] M₃) : e.trans (e.symm.trans f) = f

theorem LinearEquiv.symm_trans_cancel_left {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₂ ≃ₛₗ[σ₂₃] M₃) : e.symm.trans (e.trans f) = f

theorem LinearEquiv.trans_symm_cancel_right {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ ≃ₛₗ[σ₃₁] M₁) : (f.trans e).trans e.symm = f

theorem LinearEquiv.symm_trans_cancel_right {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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ ≃ₛₗ[σ₃₂] M₂) : (f.trans e.symm).trans e = f

@[simp]

theorem LinearEquiv.refl_symm {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] : (refl R M).symm = refl R M

@[simp]

theorem LinearEquiv.self_trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.trans f.symm = refl R₁ M₁

@[simp]

theorem LinearEquiv.symm_trans_self {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.symm.trans f = refl R₂ M₂

@[simp]

theorem LinearEquiv.refl_toLinearMap {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(refl R M) = LinearMap.id

@[simp]

theorem LinearEquiv.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ → M) (h₁ : Function.LeftInverse f (↑e).toFun) (h₂ : Function.RightInverse f (↑e).toFun) : { toLinearMap := ↑e, invFun := f, left_inv := h₁, right_inv := h₂ } = e

theorem LinearEquiv.map_add {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a b : M) : e (a + b) = e a + e b

theorem LinearEquiv.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e 0 = 0

theorem LinearEquiv.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : R) (x : M) : e (c • x) = σ c • e x

theorem LinearEquiv.map_smul {R₁ : Type u_2} {N₁ : Type u_12} {N₂ : Type u_13} [Semiring R₁] [AddCommMonoid N₁] [AddCommMonoid 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

theorem LinearEquiv.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M} : e x = 0 ↔ x = 0

theorem LinearEquiv.map_ne_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M} : e x ≠ 0 ↔ x ≠ 0

@[simp]

theorem LinearEquiv.symm_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.symm.symm = e

theorem LinearEquiv.symm_bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {σ : R →+* S} {σ' : S →+* R} [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] : Function.Bijective symm

@[simp]

theorem LinearEquiv.mk_coe' {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ → M) (h₁ : ∀ (x y : M₂), f (x + y) = f x + f y) (h₂ : ∀ (m : S) (x : M₂), { toFun := f, map_add' := h₁ }.toFun (m • x) = σ' m • { toFun := f, map_add' := h₁ }.toFun x) (h₃ : Function.LeftInverse ⇑e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun) (h₄ : Function.RightInverse ⇑e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun) : { toFun := f, map_add' := h₁, map_smul' := h₂, invFun := ⇑e, left_inv := h₃, right_inv := h₄ } = e.symm

def LinearEquiv.symm_mk.aux {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ → M) (h₁ : ∀ (x y : M), e (x + y) = e x + e y) (h₂ : ∀ (m : R) (x : M), { toFun := ⇑e, map_add' := h₁ }.toFun (m • x) = σ m • { toFun := ⇑e, map_add' := h₁ }.toFun x) (h₃ : Function.LeftInverse f { toFun := ⇑e, map_add' := h₁, map_smul' := h₂ }.toFun) (h₄ : Function.RightInverse f { toFun := ⇑e, map_add' := h₁, map_smul' := h₂ }.toFun) : M₂ ≃ₛₗ[σ'] M

Auxiliary definition to avoid looping in dsimp with LinearEquiv.symm_mk.

@[simp]

theorem LinearEquiv.symm_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ → M) (h₁ : ∀ (x y : M), e (x + y) = e x + e y) (h₂ : ∀ (m : R) (x : M), { toFun := ⇑e, map_add' := h₁ }.toFun (m • x) = σ m • { toFun := ⇑e, map_add' := h₁ }.toFun x) (h₃ : Function.LeftInverse f { toFun := ⇑e, map_add' := h₁, map_smul' := h₂ }.toFun) (h₄ : Function.RightInverse f { toFun := ⇑e, map_add' := h₁, map_smul' := h₂ }.toFun) : { toFun := ⇑e, map_add' := h₁, map_smul' := h₂, invFun := f, left_inv := h₃, right_inv := h₄ }.symm = let __src := symm_mk.aux e f h₁ h₂ h₃ h₄; { toFun := f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑e, left_inv := ⋯, right_inv := ⋯ }

theorem LinearEquiv.coe_symm_mk {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module 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), { toFun := to_fun, map_add' := map_add }.toFun (m • x) = (RingHom.id R) m • { toFun := to_fun, map_add' := map_add }.toFun x} {left_inv : Function.LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun} {right_inv : Function.RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun} : ⇑{ toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }.symm = inv_fun

For a more powerful version, see coe_symm_mk'.

@[simp]

theorem LinearEquiv.coe_symm_mk' {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M →ₗ[R] M₂} {inv_fun : M₂ → M} {left_inv : Function.LeftInverse inv_fun f.toFun} {right_inv : Function.RightInverse inv_fun f.toFun} : ⇑{ toLinearMap := f, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }.symm = inv_fun

theorem LinearEquiv.bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : Function.Bijective ⇑e

theorem LinearEquiv.injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : Function.Injective ⇑e

theorem LinearEquiv.surjective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : Function.Surjective ⇑e

theorem LinearEquiv.image_eq_preimage_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : Set M) : ⇑e '' s = ⇑e.symm ⁻¹' s

theorem LinearEquiv.image_symm_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : Set M₂) : ⇑e.symm '' s = ⇑e ⁻¹' s

def LinearEquiv.cast {R : Type u_1} [Semiring R] {ι : Type u_14} {M : ι → Type u_15} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {i j : ι} (h : i = j) : M i ≃ₗ[R] M j

Equiv.cast (congrArg _ h) as a linear equiv.

Note that unlike Equiv.cast, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

@[simp]

theorem LinearEquiv.cast_apply {R : Type u_1} [Semiring R] {ι : Type u_14} {M : ι → Type u_15} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {i j : ι} (h : i = j) (a✝ : M i) : (LinearEquiv.cast h) a✝ = cast ⋯ a✝

@[simp]

theorem LinearEquiv.cast_symm_apply {R : Type u_1} [Semiring R] {ι : Type u_14} {M : ι → Type u_15} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {i j : ι} (h : i = j) (a✝ : M j) : (LinearEquiv.cast h).symm a✝ = cast ⋯ a✝

def RingEquiv.toSemilinearEquiv {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) : R ≃ₛₗ[↑f] S

Interpret a RingEquiv f as an f-semilinear equiv.

@[simp]

theorem RingEquiv.toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) (a✝ : S) : f.toSemilinearEquiv.symm a✝ = f.invFun a✝

@[simp]

theorem RingEquiv.toSemilinearEquiv_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) (a : R) : f.toSemilinearEquiv a = f a

@[simp]

theorem RingEquiv.symm_toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) (x : R) : f.symm.toSemilinearEquiv.symm x = f x

def LinearEquiv.ofInvolutive {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {x✝ : Module R M} (f : M →ₛₗ[σ] M) (hf : Function.Involutive ⇑f) : M ≃ₛₗ[σ] M

An involutive linear map is a linear equivalence.

@[simp]

theorem LinearEquiv.coe_ofInvolutive {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {x✝ : Module R M} (f : M →ₛₗ[σ] M) (hf : Function.Involutive ⇑f) : ⇑(ofInvolutive f hf) = ⇑f

@[implicit_reducible]

instance LinearEquiv.instSMulUnitsId {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] : SMul Sˣ (V ≃ₗ[R] W)

Left scalar multiplication of a unit and a linear equivalence, as a linear equivalence.

@[simp]

theorem LinearEquiv.smul_apply {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] (α : Sˣ) (e : V ≃ₗ[R] W) (x : V) : (α • e) x = ↑α • e x

theorem LinearEquiv.symm_smul_apply {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] (e : V ≃ₗ[R] W) (α : Sˣ) (x : W) : (α • e).symm x = ↑α⁻¹ • e.symm x

@[simp]

theorem LinearEquiv.symm_smul {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] [SMulCommClass R S V] (e : V ≃ₗ[R] W) (α : Sˣ) : (α • e).symm = α⁻¹ • e.symm

@[simp]

theorem LinearEquiv.toLinearMap_smul {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] (e : V ≃ₗ[R] W) (α : Sˣ) : ↑(α • e) = ↑α • ↑e

theorem LinearEquiv.smul_trans {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} {G : Type u_18} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [AddCommMonoid G] [Module R G] [Module S G] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] [SMulCommClass R S V] [IsScalarTower S R G] (α : Sˣ) (e : G ≃ₗ[R] V) (f : V ≃ₗ[R] W) : (α • e) ≪≫ₗ f = α • e ≪≫ₗ f

theorem LinearEquiv.trans_smul {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} {G : Type u_18} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [Module S V] [AddCommMonoid W] [Module R W] [Module S W] [AddCommMonoid G] [Module R G] [Module S G] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] [IsScalarTower S R G] (α : Sˣ) (e : G ≃ₗ[R] V) (f : V ≃ₗ[R] W) : e ≪≫ₗ (α • f) = α • e ≪≫ₗ f