Further results on (semi)linear equivalences.

def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [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.

@[simp]

theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M₂) : (restrictScalars R f).symm a = f.symm a

@[simp]

theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M) : (restrictScalars R f) a = f a

theorem LinearEquiv.restrictScalars_injective (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : Function.Injective (restrictScalars R)

@[simp]

theorem LinearEquiv.restrictScalars_inj (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f g : M ≃ₗ[S] M₂) : restrictScalars R f = restrictScalars R g ↔ f = g

theorem Module.End.isUnit_iff {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) : IsUnit f ↔ Function.Bijective ⇑f

@[deprecated Module.End.isUnit_iff (since := "2025-04-28")]

theorem Module.End_isUnit_iff {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) : IsUnit f ↔ Function.Bijective ⇑f

Alias of Module.End.isUnit_iff.

instance LinearEquiv.automorphismGroup {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Group (M ≃ₗ[R] M)

theorem LinearEquiv.one_eq_refl {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : 1 = refl R M

theorem LinearEquiv.mul_eq_trans {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f g : M ≃ₗ[R] M) : f * g = g ≪≫ₗ f

@[simp]

theorem LinearEquiv.coe_one {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑1 = id

@[simp]

theorem LinearEquiv.coe_toLinearMap_one {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : ↑1 = LinearMap.id

@[simp]

theorem LinearEquiv.coe_toLinearMap_mul {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {e₁ e₂ : M ≃ₗ[R] M} : ↑(e₁ * e₂) = ↑e₁ * ↑e₂

theorem LinearEquiv.coe_pow {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (n : ℕ) : ⇑(e ^ n) = (⇑e)^[n]

theorem LinearEquiv.pow_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (n : ℕ) (m : M) : (e ^ n) m = (⇑e)^[n] m

@[simp]

theorem LinearEquiv.mul_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f g : M ≃ₗ[R] M) (x : M) : (f * g) x = f (g x)

def LinearEquiv.automorphismGroup.toLinearMapMonoidHom {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [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.

@[simp]

theorem LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) : toLinearMapMonoidHom e = ↑e

instance LinearEquiv.applyDistribMulAction {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : DistribMulAction (M ≃ₗ[R] M) M

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

This generalizes Function.End.applyMulAction.

@[simp]

theorem LinearEquiv.smul_def {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) (a : M) : f • a = f a

instance LinearEquiv.apply_faithfulSMul {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : FaithfulSMul (M ≃ₗ[R] M) M

LinearEquiv.applyDistribMulAction is faithful.

instance LinearEquiv.apply_smulCommClass {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass S (M ≃ₗ[R] M) M

instance LinearEquiv.apply_smulCommClass' {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (M ≃ₗ[R] M) S M

def LinearEquiv.ofSubsingleton {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] : M ≃ₗ[R] M₂

Any two modules that are subsingletons are isomorphic.

@[simp]

theorem LinearEquiv.ofSubsingleton_symm_apply {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] (x✝ : M₂) : (ofSubsingleton M M₂).symm x✝ = 0

@[simp]

theorem LinearEquiv.ofSubsingleton_apply {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] (x✝ : M) : (ofSubsingleton M M₂) x✝ = 0

@[simp]

theorem LinearEquiv.ofSubsingleton_self {R : Type u_1} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] : ofSubsingleton M M = refl R M

def Module.compHom.toLinearEquiv {R : Type u_9} {S : Type u_10} [Semiring R] [Semiring S] (g : R ≃+* S) : R ≃ₗ[R] S

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

@[simp]

theorem Module.compHom.toLinearEquiv_apply {R : Type u_9} {S : Type u_10} [Semiring R] [Semiring S] (g : R ≃+* S) (a : R) : (toLinearEquiv g) a = g a

@[simp]

theorem Module.compHom.toLinearEquiv_symm_apply {R : Type u_9} {S : Type u_10} [Semiring R] [Semiring S] (g : R ≃+* S) (a : S) : (toLinearEquiv g).symm a = g.symm a

def DistribMulAction.toLinearEquiv (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : M ≃ₗ[R] M

Each element of the group defines a linear equivalence.

This is a stronger version of DistribMulAction.toAddEquiv.

@[simp]

theorem DistribMulAction.toLinearEquiv_symm_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (a✝ : M) : (toLinearEquiv R M s).symm a✝ = s⁻¹ • a✝

@[simp]

theorem DistribMulAction.toLinearEquiv_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (a✝ : M) : (toLinearEquiv R M s) a✝ = s • a✝

def DistribMulAction.toModuleAut (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [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.

@[simp]

theorem DistribMulAction.toModuleAut_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : (toModuleAut R M) s = toLinearEquiv R M s

def AddEquiv.toLinearEquiv {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [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.

@[simp]

theorem AddEquiv.coe_toLinearEquiv {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c • x) = c • e x) : ⇑(e.toLinearEquiv h) = ⇑e

@[simp]

theorem AddEquiv.coe_toLinearEquiv_symm {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c • x) = c • e x) : ⇑(e.toLinearEquiv h).symm = ⇑e.symm

def AddEquiv.toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : M ≃ₗ[ℕ] M₂

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

@[simp]

theorem AddEquiv.coe_toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : ⇑e.toNatLinearEquiv = ⇑e

@[simp]

theorem AddEquiv.toNatLinearEquiv_toAddEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : ↑e.toNatLinearEquiv = e

@[simp]

theorem LinearEquiv.toAddEquiv_toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃ₗ[ℕ] M₂) : (↑e).toNatLinearEquiv = e

@[simp]

theorem AddEquiv.toNatLinearEquiv_symm {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv

@[simp]

theorem AddEquiv.toNatLinearEquiv_refl {M : Type u_5} [AddCommMonoid M] : (refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M

@[simp]

theorem AddEquiv.toNatLinearEquiv_trans {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) : e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv

def AddEquiv.toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : M ≃ₗ[ℤ] M₂

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

@[simp]

theorem AddEquiv.coe_toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : ⇑e.toIntLinearEquiv = ⇑e

@[simp]

theorem AddEquiv.toIntLinearEquiv_toAddEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : ↑e.toIntLinearEquiv = e

@[simp]

theorem LinearEquiv.toAddEquiv_toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃ₗ[ℤ] M₂) : (↑e).toIntLinearEquiv = e

@[simp]

theorem AddEquiv.toIntLinearEquiv_symm {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv

@[simp]

theorem AddEquiv.toIntLinearEquiv_refl {M : Type u_5} [AddCommGroup M] : (refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M

@[simp]

theorem AddEquiv.toIntLinearEquiv_trans {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) : e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv

def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_4) (M : Type u_5) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M

The equivalence between R-linear maps from R to M, and points of M itself. This says that the forgetful functor from R-modules to types is representable, by R.

This is an S-linear equivalence, under the assumption that S acts on M commuting with R. When R is commutative, we can take this to be the usual action with S = R. Otherwise, S = ℕ shows that the equivalence is additive. See note [bundled maps over different rings].

@[simp]

theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_4) (M : Type u_5) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : R →ₗ[R] M) : (ringLmapEquivSelf R S M) f = f 1

@[simp]

theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_4) (M : Type u_5) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (x : M) : (ringLmapEquivSelf R S M).symm x = smulRight 1 x

def addMonoidHomLequivNat {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B

The R-linear equivalence between additive morphisms A →+ B and ℕ-linear morphisms A →ₗ[ℕ] B.

@[simp]

theorem addMonoidHomLequivNat_symm_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →ₗ[ℕ] B) : (addMonoidHomLequivNat R).symm f = f.toAddMonoidHom

@[simp]

theorem addMonoidHomLequivNat_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →+ B) : (addMonoidHomLequivNat R) f = f.toNatLinearMap

def addMonoidHomLequivInt {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B

The R-linear equivalence between additive morphisms A →+ B and ℤ-linear morphisms A →ₗ[ℤ] B.

@[simp]

theorem addMonoidHomLequivInt_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →+ B) : (addMonoidHomLequivInt R) f = f.toIntLinearMap

@[simp]

theorem addMonoidHomLequivInt_symm_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →ₗ[ℤ] B) : (addMonoidHomLequivInt R).symm f = f.toAddMonoidHom

def addMonoidEndRingEquivInt (A : Type u_9) [AddCommGroup A] : AddMonoid.End A ≃+* Module.End ℤ A

Ring equivalence between additive group endomorphisms of an AddCommGroup A and ℤ-module endomorphisms of A.

@[simp]

theorem addMonoidEndRingEquivInt_apply (A : Type u_9) [AddCommGroup A] (a✝ : A →+ A) : (addMonoidEndRingEquivInt A) a✝ = (↑(addMonoidHomLequivInt ℤ)).toFun a✝

@[simp]

theorem addMonoidEndRingEquivInt_symm_apply (A : Type u_9) [AddCommGroup A] (a✝ : A →ₗ[ℤ] A) : (addMonoidEndRingEquivInt A).symm a✝ = (addMonoidHomLequivInt ℤ).invFun a✝

instance LinearEquiv.instZero {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : Zero (M ≃ₛₗ[σ₁₂] M₂)

Between two zero modules, the zero map is an equivalence.

@[simp]

theorem LinearEquiv.zero_symm {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : symm 0 = 0

@[simp]

theorem LinearEquiv.coe_zero {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : ⇑0 = 0

theorem LinearEquiv.zero_apply {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] (x : M) : 0 x = 0

instance LinearEquiv.instUnique {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : Unique (M ≃ₛₗ[σ₁₂] M₂)

Between two zero modules, the zero map is the only equivalence.

instance LinearEquiv.uniqueOfSubsingleton {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton R] [Subsingleton R₂] : Unique (M ≃ₛₗ[σ₁₂] M₂)

def LinearEquiv.curry (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_9) (V₂ : Type u_10) : (V × V₂ → M) ≃ₗ[R] V → V₂ → M

Linear equivalence between a curried and uncurried function. Differs from TensorProduct.curry.

@[simp]

theorem LinearEquiv.coe_curry (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_9) (V₂ : Type u_10) : ⇑(LinearEquiv.curry R M V V₂) = Function.curry

@[simp]

theorem LinearEquiv.coe_curry_symm (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_9) (V₂ : Type u_10) : ⇑(LinearEquiv.curry R M V V₂).symm = Function.uncurry

def LinearEquiv.ofLinear {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [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₂) (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂

If a linear map has an inverse, it is a linear equivalence.

@[simp]

theorem LinearEquiv.ofLinear_apply {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [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₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} (x : M) : (ofLinear f g h₁ h₂) x = f x

@[simp]

theorem LinearEquiv.ofLinear_symm_apply {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [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₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} (x : M₂) : (ofLinear f g h₁ h₂).symm x = g x

@[simp]

theorem LinearEquiv.ofLinear_toLinearMap {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [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₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} : ↑(ofLinear f g h₁ h₂) = f

@[simp]

theorem LinearEquiv.ofLinear_symm_toLinearMap {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [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₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} : ↑(ofLinear f g h₁ h₂).symm = g

def LinearEquiv.neg (R : Type u_1) {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] : M ≃ₗ[R] M

x ↦ -x as a LinearEquiv

@[simp]

theorem LinearEquiv.coe_neg {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] : ⇑(neg R) = -id

theorem LinearEquiv.neg_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] (x : M) : (neg R) x = -x

@[simp]

theorem LinearEquiv.symm_neg {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] : (neg R).symm = neg R

def LinearEquiv.arrowCongrAddEquiv {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃+ (M₂ →ₗ[R] M₂₂)

A linear isomorphism between the domains and codomains of two spaces of linear maps gives an additive isomorphism between the two function spaces.

See also LinearEquiv.arrowCongr for the linear version of this isomorphism.

@[simp]

theorem LinearEquiv.arrowCongrAddEquiv_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) : (e₁.arrowCongrAddEquiv e₂) f = ↑e₂ ∘ₗ f ∘ₗ ↑e₁.symm

@[simp]

theorem LinearEquiv.arrowCongrAddEquiv_symm_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) : (e₁.arrowCongrAddEquiv e₂).symm f = ↑e₂.symm ∘ₗ f ∘ₗ ↑e₁

def LinearEquiv.domMulActCongrRight {R : Type u_1} {S : Type u_4} {M₁ : Type u_6} {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₂₂] [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[Sᵈᵐᵃ] M₁ →ₗ[R] M₂₂

A linear isomorphism between the domains an codomains of two spaces of linear maps gives a linear isomorphism with respect to an action on the domains.

@[simp]

theorem LinearEquiv.domMulActCongrRight_apply {R : Type u_1} {S : Type u_4} {M₁ : Type u_6} {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₂₂] [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) (a✝ : M₁ →ₗ[R] M₂₁) : e₂.domMulActCongrRight a✝ = ((refl R M₁).arrowCongrAddEquiv e₂).toFun a✝

@[simp]

theorem LinearEquiv.domMulActCongrRight_symm_apply {R : Type u_1} {S : Type u_4} {M₁ : Type u_6} {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₂₂] [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) (a✝ : M₁ →ₗ[R] M₂₂) : e₂.domMulActCongrRight.symm a✝ = ((refl R M₁).arrowCongrAddEquiv e₂).invFun a✝

def LinearEquiv.conjRingEquiv {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) : Module.End R M₁ ≃+* Module.End R M₂

If M and M₂ are linearly isomorphic then the endomorphism rings of M and M₂ are isomorphic.

See LinearEquiv.conj for the linear version of this isomorphism.

@[simp]

theorem LinearEquiv.conjRingEquiv_apply_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : M₁ →ₗ[R] M₁) (a✝ : M₂) : (e.conjRingEquiv f) a✝ = e (f (e.symm a✝))

@[simp]

theorem LinearEquiv.conjRingEquiv_symm_apply_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : M₂ →ₗ[R] M₂) (a✝ : M₁) : (e.conjRingEquiv.symm f) a✝ = e.symm (f (e a✝))

def LinearEquiv.smulOfUnit {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : Rˣ) : M ≃ₗ[R] M

Multiplying by a unit a of the ring R is a linear equivalence.

def LinearEquiv.arrowCongr {R : Type u_9} {M₁ : Type u_10} {M₂ : Type u_11} {M₂₁ : Type u_12} {M₂₂ : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂

A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces.

See LinearEquiv.arrowCongrAddEquiv for the additive version of this isomorphism that works over a not necessarily commutative semiring.

@[simp]

theorem LinearEquiv.arrowCongr_apply {R : Type u_9} {M₁ : Type u_10} {M₂ : Type u_11} {M₂₁ : Type u_12} {M₂₂ : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) (x : M₂) : ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))

@[simp]

theorem LinearEquiv.arrowCongr_symm_apply {R : Type u_9} {M₁ : Type u_10} {M₂ : Type u_11} {M₂₁ : Type u_12} {M₂₂ : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) : ((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))

theorem LinearEquiv.arrowCongr_comp {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {N : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : (e₁.arrowCongr e₃) (g ∘ₗ f) = (e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f

theorem LinearEquiv.arrowCongr_trans {R : Type u_1} [CommSemiring R] {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} {N₃ : Type u_14} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) : e₁.arrowCongr e₂ ≪≫ₗ e₃.arrowCongr e₄ = (e₁ ≪≫ₗ e₃).arrowCongr (e₂ ≪≫ₗ e₄)

def LinearEquiv.congrRight {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ[R] M →ₗ[R] M₃

If M₂ and M₃ are linearly isomorphic then the two spaces of linear maps from M into M₂ and M into M₃ are linearly isomorphic.

def LinearEquiv.conj {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) : Module.End R M ≃ₗ[R] Module.End R M₂

If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to themselves are linearly isomorphic.

See LinearEquiv.conjRingEquiv for the isomorphism between endomorphism rings, which works over a not necessarily commutative semiring.

theorem LinearEquiv.conj_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) : e.conj f = (↑e ∘ₗ f) ∘ₗ ↑e.symm

theorem LinearEquiv.conj_apply_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) : (e.conj f) x = e (f (e.symm x))

theorem LinearEquiv.symm_conj_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) : e.symm.conj f = (↑e.symm ∘ₗ f) ∘ₗ ↑e

theorem LinearEquiv.conj_comp {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f g : Module.End R M) : e.conj (g ∘ₗ f) = e.conj g ∘ₗ e.conj f

theorem LinearEquiv.conj_trans {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : e₁.conj ≪≫ₗ e₂.conj = (e₁ ≪≫ₗ e₂).conj

@[simp]

theorem LinearEquiv.conj_conj_symm {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) : e.conj (e.symm.conj f) = f

@[simp]

theorem LinearEquiv.conj_symm_conj {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) : e.symm.conj (e.conj f) = f

@[simp]

theorem LinearEquiv.conj_id {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id

@[simp]

theorem LinearEquiv.conj_refl {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) : (refl R M).conj f = f

def LinearEquiv.congrLeft (M : Type u_5) {M₂ : Type u_7} {M₃ : Type u_8} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {R : Type u_9} (S : Type u_10) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) : (M₂ →ₗ[R] M) ≃ₗ[S] M₃ →ₗ[R] M

An R-linear isomorphism between two R-modules M₂ and M₃ induces an S-linear isomorphism between M₂ →ₗ[R] M and M₃ →ₗ[R] M, if M is both an R-module and an S-module and their actions commute.

def LinearEquiv.smulOfNeZero (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M

Multiplying by a nonzero element a of the field K is a linear equivalence.

@[simp]

theorem LinearEquiv.smulOfNeZero_apply (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) (a✝ : M) : (smulOfNeZero K M a ha) a✝ = a • a✝

@[simp]

theorem LinearEquiv.smulOfNeZero_symm_apply (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) (a✝ : M) : (smulOfNeZero K M a ha).symm a✝ = (Units.mk0 a ha)⁻¹ • a✝

def Equiv.toLinearEquiv {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (e : M ≃ M₂) (h : IsLinearMap R ⇑e) : M ≃ₗ[R] M₂

An equivalence whose underlying function is linear is a linear equivalence.

def LinearMap.funLeft (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) : (n → M) →ₗ[R] m → M

Given an R-module M and a function m → n between arbitrary types, construct a linear map (n → M) →ₗ[R] (m → M)

@[simp]

theorem LinearMap.funLeft_apply (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) (g : n → M) (i : m) : (funLeft R M f) g i = g (f i)

@[simp]

theorem LinearMap.funLeft_id (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_10} (g : n → M) : (funLeft R M _root_.id) g = g

theorem LinearMap.funLeft_comp (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} {p : Type u_11} (f₁ : n → p) (f₂ : m → n) : funLeft R M (f₁ ∘ f₂) = funLeft R M f₂ ∘ₗ funLeft R M f₁

theorem LinearMap.funLeft_surjective_of_injective (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) (hf : Function.Injective f) : Function.Surjective ⇑(funLeft R M f)

theorem LinearMap.funLeft_injective_of_surjective (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) (hf : Function.Surjective f) : Function.Injective ⇑(funLeft R M f)

def LinearEquiv.funCongrLeft (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (e : m ≃ n) : (n → M) ≃ₗ[R] m → M

Given an R-module M and an equivalence m ≃ n between arbitrary types, construct a linear equivalence (n → M) ≃ₗ[R] (m → M)

@[simp]

theorem LinearEquiv.funCongrLeft_apply (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (e : m ≃ n) (x : n → M) : (funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x

@[simp]

theorem LinearEquiv.funCongrLeft_id (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_10} : funCongrLeft R M (Equiv.refl n) = refl R (n → M)

@[simp]

theorem LinearEquiv.funCongrLeft_comp (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} {p : Type u_11} (e₁ : m ≃ n) (e₂ : n ≃ p) : funCongrLeft R M (e₁.trans e₂) = funCongrLeft R M e₂ ≪≫ₗ funCongrLeft R M e₁

@[simp]

theorem LinearEquiv.funCongrLeft_symm (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (e : m ≃ n) : (funCongrLeft R M e).symm = funCongrLeft R M e.symm

def LinearEquiv.sumPiEquivProdPi (R : Type u_9) [Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] : ((st : S ⊕ T) → A st) ≃ₗ[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))

The product over S ⊕ T of a family of modules is isomorphic to the product of (the product over S) and (the product over T).

This is Equiv.sumPiEquivProdPi as a LinearEquiv.

@[simp]

theorem LinearEquiv.sumPiEquivProdPi_apply (R : Type u_9) [Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] : ⇑(sumPiEquivProdPi R S T A) = ⇑(Equiv.sumPiEquivProdPi A)

@[simp]

theorem LinearEquiv.sumPiEquivProdPi_symm_apply (R : Type u_9) [Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] : ⇑(sumPiEquivProdPi R S T A).symm = ⇑(Equiv.sumPiEquivProdPi A).symm

def LinearEquiv.piUnique {α : Type u_9} [Unique α] (R : Type u_10) [Semiring R] (f : α → Type u_11) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] : ((t : α) → f t) ≃ₗ[R] f default

The product Π t : α, f t of a family of modules is linearly isomorphic to the module f ⬝ when α only contains ⬝.

This is Equiv.piUnique as a LinearEquiv.

@[simp]

theorem LinearEquiv.piUnique_symm_apply {α : Type u_9} [Unique α] (R : Type u_10) [Semiring R] (f : α → Type u_11) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] : ⇑(piUnique R f).symm = (Equiv.piUnique f).invFun

@[simp]

theorem LinearEquiv.piUnique_apply {α : Type u_9} [Unique α] (R : Type u_10) [Semiring R] (f : α → Type u_11) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] : ⇑(piUnique R f) = (Equiv.piUnique f).toFun