Theorems · Definition · ring theory

toModuleCatFromModuleCatLinearEquiv

(R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (M : ModuleCat (Matrix ι ι R)) → (j : ι) → ↑M ≃ₗ[Matrix ι ι R] ι → ↥(MatrixModCat.toModuleCatObj R (↑M) j)

The linear equiv induced by the equality toMatrixModCat (toModuleCat M) = Mⁿ

Defined in

Mathlib.RingTheory.Morita.Matrix

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingFintypeDecidableEq