Documentation

Mathlib.Algebra.Module.Equiv

(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_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (σ : R →+* S) {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] (M : Type u_3) (M₂ : Type u_4) [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] extends LinearMap :
Type (maxu_3u_4)
  • The backwards directed function underlying a linear equivalence.

    invFun : M₂M
  • LinearEquiv.invFun is a left inverse to the linear equivalence's underlying function.

    left_inv : Function.LeftInverse invFun toLinearMap.toAddHom.toFun
  • LinearEquiv.invFun is a right inverse to the linear equivalence's underlying function.

    right_inv : Function.RightInverse invFun toLinearMap.toAddHom.toFun

A linear equivalence is an invertible linear map.

Instances For
    abbrev LinearEquiv.toAddEquiv {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] {M : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] (self : M ≃ₛₗ[σ] M₂) :
    M ≃+ M₂

    The additive equivalence of types underlying a linear equivalence.

    Equations
    • One or more equations did not get rendered due to their size.

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

    Equations
    • One or more equations did not get rendered due to their size.

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

    Equations
    • One or more equations did not get rendered due to their size.

    The notation M ≃ₗ⋆[R] M₂≃ₗ⋆[R] M₂⋆[R] M₂ denotes the type of star-linear equivalences between M and M₂ over the ⋆⋆ endomorphism of the underlying starred ring R.

    Equations
    • One or more equations did not get rendered due to their size.
    class SemilinearEquivClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst : Semiring S] (σ : outParam (R →+* S)) {σ' : outParam (S →+* R)} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] (M : outParam (Type u_4)) (M₂ : outParam (Type u_5)) [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] extends AddEquivClass :
    Type (max(maxu_1u_4)u_5)
    • Applying a semilinear equivalence f over σ to r • x equals σ r • f x.

      map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r x) = σ r f x

    SemilinearEquivClass F σ M M₂ asserts F is a type of bundled σ-semilinear equivs M → 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→+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

    Instances
      @[inline]
      abbrev LinearEquivClass (F : Type u_1) (R : outParam (Type u_2)) (M : outParam (Type u_3)) (M₂ : outParam (Type u_4)) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] :
      Type (max(maxu_1u_3)u_4)

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

      Equations
      @[infer_tc_goals_rl]
      instance SemilinearEquivClass.instSemilinearMapClass {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} (F : Type u_5) [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] [s : SemilinearEquivClass F σ M M₂] :
      SemilinearMapClass F σ M M₂
      Equations
      instance LinearEquiv.instCoeLinearEquivLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)
      Equations
      • LinearEquiv.instCoeLinearEquivLinearMap = { coe := LinearEquiv.toLinearMap }
      def LinearEquiv.toEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      (M ≃ₛₗ[σ] M₂) → M M₂

      The equivalence of types underlying a linear equivalence.

      Equations
      theorem LinearEquiv.toEquiv_injective {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      Function.Injective LinearEquiv.toEquiv
      @[simp]
      theorem LinearEquiv.toEquiv_inj {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] {e₁ : M ≃ₛₗ[σ] M₂} {e₂ : M ≃ₛₗ[σ] M₂} :
      theorem LinearEquiv.toLinearMap_injective {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      Function.Injective LinearEquiv.toLinearMap
      @[simp]
      theorem LinearEquiv.toLinearMap_inj {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] {e₁ : M ≃ₛₗ[σ] M₂} {e₂ : M ≃ₛₗ[σ] M₂} :
      e₁ = e₂ e₁ = e₂
      instance LinearEquiv.instSemilinearEquivClassLinearEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem LinearEquiv.coe_mk {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] {to_fun : MM₂} {inv_fun : M₂M} {map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y} {map_smul : ∀ (r : R) (x : M), AddHom.toFun { toFun := to_fun, map_add' := map_add } (r x) = σ r AddHom.toFun { toFun := to_fun, map_add' := map_add } x} {left_inv : Function.LeftInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} {right_inv : Function.RightInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} :
      { toLinearMap := { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv } = to_fun
      theorem LinearEquiv.coe_injective {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      @[simp]
      theorem LinearEquiv.coe_coe {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
      @[simp]
      theorem LinearEquiv.coe_toLinearMap {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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).toAddHom.toFun = e
      theorem LinearEquiv.ext {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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' : M ≃ₛₗ[σ] M₂} (h : ∀ (x : M), e x = e' x) :
      e = e'
      theorem LinearEquiv.ext_iff {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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' : M ≃ₛₗ[σ] M₂} :
      e = e' ∀ (x : M), e x = e' x
      theorem LinearEquiv.congr_arg {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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} {x' : M} :
      x = x'e x = e x'
      theorem LinearEquiv.congr_fun {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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' : M ≃ₛₗ[σ] M₂} (h : e = e') (x : M) :
      e x = e' x
      def LinearEquiv.refl (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

      The identity map is a linear equivalence.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem LinearEquiv.refl_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
      ↑(LinearEquiv.refl R M) x = x
      def LinearEquiv.symm {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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
      • One or more equations did not get rendered due to their size.
      def LinearEquiv.Simps.apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] {M : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] (e : M ≃ₛₗ[σ] M₂) :
      MM₂

      See Note [custom simps projection]

      Equations
      def LinearEquiv.Simps.symm_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] {σ : R →+* S} {σ' : S →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] {M : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] (e : M ≃ₛₗ[σ] M₂) :
      M₂M

      See Note [custom simps projection]

      Equations
      @[simp]
      theorem LinearEquiv.invFun_eq_symm {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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 = ↑(LinearEquiv.symm e)
      @[simp]
      theorem LinearEquiv.coe_toEquiv_symm {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_1} {R₂ : Type u_2} {R₃ : Type u_3} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [inst : RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [inst : RingHomInvPair σ₃₁ σ₁₃] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
      M₁ ≃ₛₗ[σ₁₃] M₃

      Linear equivalences are transitive.

      Equations
      • One or more equations did not get rendered due to their size.

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

      Equations
      @[simp]
      theorem LinearEquiv.coe_toAddEquiv {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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.toAddMonoidHom_commutes {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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

      @[simp]
      theorem LinearEquiv.trans_apply {R₁ : Type u_3} {R₂ : Type u_5} {R₃ : Type u_4} {M₁ : Type u_2} {M₂ : Type u_6} {M₃ : Type u_1} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [inst : RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [inst : RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₁) :
      ↑(LinearEquiv.trans e₁₂ e₂₃) c = e₂₃ (e₁₂ c)
      theorem LinearEquiv.coe_trans {R₁ : Type u_3} {R₂ : Type u_5} {R₃ : Type u_4} {M₁ : Type u_1} {M₂ : Type u_6} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [inst : RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [inst : RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
      ↑(LinearEquiv.trans e₁₂ e₂₃) = LinearMap.comp e₂₃ e₁₂
      @[simp]
      theorem LinearEquiv.apply_symm_apply {R : Type u_4} {S : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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 (↑(LinearEquiv.symm e) c) = c
      @[simp]
      theorem LinearEquiv.symm_apply_apply {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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) :
      ↑(LinearEquiv.symm e) (e b) = b
      @[simp]
      theorem LinearEquiv.trans_symm {R₁ : Type u_4} {R₂ : Type u_5} {R₃ : Type u_3} {M₁ : Type u_1} {M₂ : Type u_6} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [inst : RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [inst : RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
      theorem LinearEquiv.symm_trans_apply {R₁ : Type u_4} {R₂ : Type u_5} {R₃ : Type u_3} {M₁ : Type u_1} {M₂ : Type u_6} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [inst : RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [inst : RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₃) :
      ↑(LinearEquiv.symm (LinearEquiv.trans e₁₂ e₂₃)) c = ↑(LinearEquiv.symm e₁₂) (↑(LinearEquiv.symm e₂₃) c)
      @[simp]
      theorem LinearEquiv.trans_refl {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
      @[simp]
      theorem LinearEquiv.refl_trans {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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.symm_apply_eq {R : Type u_4} {S : Type u_3} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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 : (fun x => M) x} :
      ↑(LinearEquiv.symm e) x = y x = e y
      theorem LinearEquiv.eq_symm_apply {R : Type u_4} {S : Type u_3} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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 : (fun x => M) x} :
      y = ↑(LinearEquiv.symm e) x e y = x
      theorem LinearEquiv.eq_comp_symm {R₁ : Type u_5} {R₂ : Type u_4} {M₁ : Type u_3} {M₂ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M₁] [inst : 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_1} (f : M₂α) (g : M₁α) :
      f = g ↑(LinearEquiv.symm e₁₂) f e₁₂ = g
      theorem LinearEquiv.comp_symm_eq {R₁ : Type u_5} {R₂ : Type u_4} {M₁ : Type u_3} {M₂ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M₁] [inst : 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_1} (f : M₂α) (g : M₁α) :
      g ↑(LinearEquiv.symm e₁₂) = f g = f e₁₂
      theorem LinearEquiv.eq_symm_comp {R₁ : Type u_5} {R₂ : Type u_4} {M₁ : Type u_2} {M₂ : Type u_3} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M₁] [inst : 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_1} (f : αM₁) (g : αM₂) :
      f = ↑(LinearEquiv.symm e₁₂) g e₁₂ f = g
      theorem LinearEquiv.symm_comp_eq {R₁ : Type u_5} {R₂ : Type u_4} {M₁ : Type u_2} {M₂ : Type u_3} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M₁] [inst : 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_1} (f : αM₁) (g : αM₂) :
      ↑(LinearEquiv.symm e₁₂) g = f g = e₁₂ f
      theorem LinearEquiv.eq_comp_toLinearMap_symm {R₁ : Type u_5} {R₂ : Type u_1} {R₃ : Type u_2} {M₁ : Type u_6} {M₂ : Type u_3} {M₃ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [inst : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
      f = LinearMap.comp g ↑(LinearEquiv.symm e₁₂) LinearMap.comp f e₁₂ = g
      theorem LinearEquiv.comp_toLinearMap_symm_eq {R₁ : Type u_5} {R₂ : Type u_1} {R₃ : Type u_2} {M₁ : Type u_6} {M₂ : Type u_3} {M₃ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [inst : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
      LinearMap.comp g ↑(LinearEquiv.symm e₁₂) = f g = LinearMap.comp f e₁₂
      theorem LinearEquiv.eq_toLinearMap_symm_comp {R₁ : Type u_2} {R₂ : Type u_5} {R₃ : Type u_1} {M₁ : Type u_4} {M₂ : Type u_6} {M₃ : Type u_3} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [inst : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
      f = LinearMap.comp (↑(LinearEquiv.symm e₁₂)) g LinearMap.comp (e₁₂) f = g
      theorem LinearEquiv.toLinearMap_symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_5} {R₃ : Type u_1} {M₁ : Type u_4} {M₂ : Type u_6} {M₃ : Type u_3} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : 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₁} [inst : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [inst : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
      LinearMap.comp (↑(LinearEquiv.symm e₁₂)) g = f g = LinearMap.comp (e₁₂) f
      @[simp]
      theorem LinearEquiv.refl_symm {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
      @[simp]
      theorem LinearEquiv.self_trans_symm {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
      @[simp]
      theorem LinearEquiv.symm_trans_self {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
      @[simp]
      theorem LinearEquiv.refl_toLinearMap {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
      ↑(LinearEquiv.refl R M) = LinearMap.id
      @[simp]
      theorem LinearEquiv.comp_coe {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module R M₂] [inst : Module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
      LinearMap.comp f' f = ↑(LinearEquiv.trans f f')
      @[simp]
      theorem LinearEquiv.mk_coe {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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).toAddHom.toFun) (h₂ : Function.RightInverse f (e).toAddHom.toFun) :
      { toLinearMap := e, invFun := f, left_inv := h₁, right_inv := h₂ } = e
      theorem LinearEquiv.map_add {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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) (b : M) :
      e (a + b) = e a + e b
      theorem LinearEquiv.map_zero {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_2} {S : Type u_4} {M : Type u_3} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_1} {N₁ : Type u_2} {N₂ : Type u_3} [inst : Semiring R₁] [inst : AddCommMonoid N₁] [inst : 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_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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.symm_bijective {R : Type u_1} {S : Type u_3} {M : Type u_2} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] {σ : R →+* S} {σ' : S →+* R} [inst : Module R M] [inst : Module S M₂] [inst : RingHomInvPair σ' σ] [inst : RingHomInvPair σ σ'] :
      Function.Bijective LinearEquiv.symm
      @[simp]
      theorem LinearEquiv.mk_coe' {R : Type u_4} {S : Type u_3} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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₂ : ∀ (r : S) (x : M₂), AddHom.toFun { toFun := f, map_add' := h₁ } (r x) = σ' r AddHom.toFun { toFun := f, map_add' := h₁ } x) (h₃ : Function.LeftInverse e { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) (h₄ : Function.RightInverse e { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) :
      { toLinearMap := { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }, invFun := e, left_inv := h₃, right_inv := h₄ } = LinearEquiv.symm e
      @[simp]
      theorem LinearEquiv.symm_mk {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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₂ : ∀ (r : R) (x : M), AddHom.toFun { toFun := e, map_add' := h₁ } (r x) = σ r AddHom.toFun { toFun := e, map_add' := h₁ } x) (h₃ : Function.LeftInverse f { toAddHom := { toFun := e, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) (h₄ : Function.RightInverse f { toAddHom := { toFun := e, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) :
      LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := e, map_add' := h₁ }, map_smul' := h₂ }, invFun := f, left_inv := h₃, right_inv := h₄ } = let src := LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := e, map_add' := h₁ }, map_smul' := h₂ }, invFun := f, left_inv := h₃, right_inv := h₄ }; { toLinearMap := { toAddHom := { toFun := f, map_add' := (_ : ∀ (x y : M₂), AddHom.toFun (src).toAddHom (x + y) = AddHom.toFun (src).toAddHom x + AddHom.toFun (src).toAddHom y) }, map_smul' := (_ : ∀ (r : S) (x : M₂), AddHom.toFun (src).toAddHom (r x) = σ' r AddHom.toFun (src).toAddHom x) }, invFun := e, left_inv := (_ : Function.LeftInverse src.invFun (src).toAddHom.toFun), right_inv := (_ : Function.RightInverse src.invFun (src).toAddHom.toFun) }
      @[simp]
      theorem LinearEquiv.coe_symm_mk {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : 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 : ∀ (r : R) (x : M), AddHom.toFun { toFun := to_fun, map_add' := map_add } (r x) = ↑(RingHom.id R) r AddHom.toFun { toFun := to_fun, map_add' := map_add } x} {left_inv : Function.LeftInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} {right_inv : Function.RightInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} :
      ↑(LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }) = inv_fun
      theorem LinearEquiv.bijective {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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 = ↑(LinearEquiv.symm e) ⁻¹' s
      theorem LinearEquiv.image_symm_eq_preimage {R : Type u_4} {S : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : 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₂) :
      ↑(LinearEquiv.symm e) '' s = e ⁻¹' s
      @[simp]
      theorem RingEquiv.toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R ≃+* S) :
      ∀ (a : S), ↑(LinearEquiv.symm (RingEquiv.toSemilinearEquiv f)) a = Equiv.invFun f.toEquiv a
      @[simp]
      theorem RingEquiv.toSemilinearEquiv_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R ≃+* S) (a : R) :
      def RingEquiv.toSemilinearEquiv {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R ≃+* S) :
      R ≃ₛₗ[f] S

      Interpret a RingEquiv f as an f-semilinear equiv.

      Equations
      • One or more equations did not get rendered due to their size.
      def LinearEquiv.ofInvolutive {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] {σ : R →+* R} {σ' : R →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      {x : Module R M} → (f : M →ₛₗ[σ] M) → Function.Involutive fM ≃ₛₗ[σ] M

      An involutive linear map is a linear equivalence.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem LinearEquiv.coe_ofInvolutive {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] {σ : R →+* R} {σ' : R →+* R} [inst : RingHomInvPair σ σ'] [inst : RingHomInvPair σ' σ] :
      ∀ {x : Module R M} (f : M →ₛₗ[σ] M) (hf : Function.Involutive f), ↑(LinearEquiv.ofInvolutive f hf) = f
      @[simp]
      theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M₂) :
      @[simp]
      theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M) :
      ↑(LinearEquiv.restrictScalars R f) a = f a
      def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) :
      M ≃ₗ[R] M₂

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

      See also LinearMap.restrictScalars.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem LinearEquiv.restrictScalars_injective (R : Type u_4) {S : Type u_3} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] :
      @[simp]
      theorem LinearEquiv.restrictScalars_inj (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (g : M ≃ₗ[S] M₂) :
      instance LinearEquiv.automorphismGroup {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
      Equations
      @[simp]
      theorem LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (e : M ≃ₗ[R] M) :
      LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = e
      def LinearEquiv.automorphismGroup.toLinearMapMonoidHom {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
      (M ≃ₗ[R] M) →* M →ₗ[R] M

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

      Equations
      • One or more equations did not get rendered due to their size.
      instance LinearEquiv.applyDistribMulAction {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

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

      This generalizes Function.End.applyMulAction.

      Equations
      @[simp]
      theorem LinearEquiv.smul_def {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (f : M ≃ₗ[R] M) (a : M) :
      f a = f a
      @[simp]
      theorem LinearEquiv.ofSubsingleton_symm_apply {R : Type u_1} (M : Type u_2) (M₂ : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Subsingleton M] [inst : Subsingleton M₂] :
      ∀ (x : M₂), ↑(LinearEquiv.symm (LinearEquiv.ofSubsingleton M M₂)) x = 0
      @[simp]
      theorem LinearEquiv.ofSubsingleton_apply {R : Type u_1} (M : Type u_2) (M₂ : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Subsingleton M] [inst : Subsingleton M₂] :
      ∀ (x : M), ↑(LinearEquiv.ofSubsingleton M M₂) x = 0
      def LinearEquiv.ofSubsingleton {R : Type u_1} (M : Type u_2) (M₂ : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Subsingleton M] [inst : Subsingleton M₂] :
      M ≃ₗ[R] M₂

      Any two modules that are subsingletons are isomorphic.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem LinearEquiv.ofSubsingleton_self {R : Type u_2} (M : Type u_1) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Subsingleton M] :
      @[simp]
      theorem Module.compHom.toLinearEquiv_symm_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (g : R ≃+* S) (a : S) :
      @[simp]
      theorem Module.compHom.toLinearEquiv_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (g : R ≃+* S) (a : R) :
      def Module.compHom.toLinearEquiv {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (g : R ≃+* S) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem DistribMulAction.toLinearEquiv_symm_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Group S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :
      @[simp]
      theorem DistribMulAction.toLinearEquiv_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Group S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :
      ∀ (a : M), ↑(DistribMulAction.toLinearEquiv R M s) a = SMul.smul s a
      def DistribMulAction.toLinearEquiv (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Group S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :

      Each element of the group defines a linear equivalence.

      This is a stronger version of DistribMulAction.toAddEquiv.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem DistribMulAction.toModuleAut_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Group S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :
      def DistribMulAction.toModuleAut (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Group S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] :
      S →* M ≃ₗ[R] M

      Each element of the group defines a module automorphism.

      This is a stronger version of DistribMulAction.toAddAut.

      Equations
      • One or more equations did not get rendered due to their size.
      def AddEquiv.toLinearEquiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
      M ≃ₗ[R] M₂

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem AddEquiv.coe_toLinearEquiv {R : Type u_2} {M : Type u_3} {M₂ : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
      @[simp]
      theorem AddEquiv.coe_toLinearEquiv_symm {R : Type u_2} {M : Type u_3} {M₂ : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
      def AddEquiv.toNatLinearEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] (e : M ≃+ M₂) :

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

      Equations
      @[simp]
      theorem AddEquiv.coe_toNatLinearEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] (e : M ≃+ M₂) :
      @[simp]
      theorem AddEquiv.toNatLinearEquiv_toAddEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] (e : M ≃+ M₂) :
      @[simp]
      theorem LinearEquiv.toAddEquiv_toNatLinearEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] (e : M ≃ₗ[] M₂) :
      @[simp]
      theorem AddEquiv.toNatLinearEquiv_trans {M : Type u_3} {M₂ : Type u_1} {M₃ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
      def AddEquiv.toIntLinearEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] (e : M ≃+ M₂) :

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

      Equations
      @[simp]
      theorem AddEquiv.coe_toIntLinearEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] (e : M ≃+ M₂) :
      @[simp]
      theorem AddEquiv.toIntLinearEquiv_toAddEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] (e : M ≃+ M₂) :
      @[simp]
      theorem LinearEquiv.toAddEquiv_toIntLinearEquiv {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] (e : M ≃ₗ[] M₂) :
      @[simp]
      theorem AddEquiv.toIntLinearEquiv_trans {M : Type u_3} {M₂ : Type u_1} {M₃ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] [inst : AddCommGroup M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :