Theorems · Definition · nonassociative algebras

Matrix.reindexLieEquiv

{R : Type u} →
  [inst : CommRing R] →
    {n : Type w} →
      [inst_1 : DecidableEq n] →
        [inst_2 : Fintype n] →
          {m : Type w₁} → [inst_3 : DecidableEq m] → [inst_4 : Fintype m] → n ≃ m → Matrix n n R ≃ₗ⁅R⁆ Matrix m m R

For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types, Matrix.reindex, is an equivalence of Lie algebras.

Defined in

Mathlib.Algebra.Lie.Matrix

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintypeDecidableEqFintype