Documentation

Mathlib.Algebra.Module.Equiv.Defs

(Semi)linear equivalences #

In this file we define

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 #

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.

Instances For

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

    Equations
      Instances For

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

        Equations
          Instances For
            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₂ :

            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.

            Instances
              @[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₂] :

              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₂.

              Equations
                Instances For
                  @[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.

                  Equations
                    Instances For
                      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.

                      Equations
                        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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :
                        Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)
                        Equations
                          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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :
                          (M ≃ₛₗ[σ] M₂) → M M₂

                          The equivalence of types underlying a linear equivalence.

                          Equations
                            Instances For
                              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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :
                              @[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₂] [Module R M] [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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :
                              @[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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} :
                              e₁ = e₂ e₁ = e₂
                              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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :
                              EquivLike (M ≃ₛₗ[σ] M₂) M M₂
                              Equations
                                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₂] [Module R M] [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₂] [Module R M] [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₂] [Module R M] [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₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :
                                @[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₂] [Module R M] [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] :

                                The identity map is a linear equivalence.

                                Equations
                                  Instances For
                                    @[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.

                                    Equations
                                      Instances For
                                        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₂) :
                                        MM₂

                                        See Note [custom simps projection]

                                        Equations
                                          Instances For
                                            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]

                                            Equations
                                              Instances For
                                                @[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
                                                @[simp]
                                                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₂) :
                                                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.

                                                Equations
                                                  Instances For

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

                                                    Equations
                                                      Instances For

                                                        Pretty printer defined by notation3 command.

                                                        Equations
                                                          Instances For
                                                            @[simp]
                                                            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₂) :

                                                            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
                                                            @[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
                                                            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] :
                                                            @[simp]
                                                            theorem LinearEquiv.comp_coe {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
                                                            f' ∘ₗ f = (f ≪≫ₗ f')
                                                            @[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 σ σ'] :
                                                            @[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.

                                                            Equations
                                                              Instances For
                                                                @[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 := }
                                                                @[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₂] {to_fun : MM₂} {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
                                                                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₂) :
                                                                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₂) :
                                                                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₂) :
                                                                theorem LinearEquiv.image_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 '' 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 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.

                                                                Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem RingEquiv.toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) (a✝ : S) :
                                                                    @[simp]
                                                                    theorem RingEquiv.toSemilinearEquiv_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) (a : R) :
                                                                    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) :

                                                                    An involutive linear map is a linear equivalence.

                                                                    Equations
                                                                      Instances For
                                                                        @[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