Theorems · Definition · nonassociative algebras

Matrix.lieConj

{R : Type u} →
  [inst : CommRing R] →
    {n : Type w} →
      [inst_1 : DecidableEq n] →
        [inst_2 : Fintype n] → (P : Matrix n n R) → Invertible P → Matrix n n R ≃ₗ⁅R⁆ Matrix n n R

An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself.

Defined in

Mathlib.Algebra.Lie.Matrix

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype