Theorems · Definition · commutative algebra

LinearEquiv.congrLeft

(M : Type u_5) →
  {M₂ : Type u_7} →
    {M₃ : Type u_8} →
      [inst : AddCommMonoid M] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : AddCommMonoid M₃] →
            {R : Type u_9} →
              (S : Type u_10) →
                [inst_3 : Semiring R] →
                  [inst_4 : Semiring S] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : Module R M] →
                          [inst_8 : Module S M] →
                            [inst_9 : SMulCommClass R S M] → (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.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

8 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoidAddCommMonoidAddCommMonoidSemiringSemiringModuleModuleModuleModuleSMulCommClass