Theorems · Definition · commutative algebra

LinearEquiv.congrRight

{R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      {M₃ : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R M₃] → (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.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModule