Commit 2023-06-03 08:32 533e6e46

View on Github →

feat: port Algebra.Lie.Matrix (#4621)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Matrix.lean

added def Matrix.lieConj

added theorem Matrix.lieConj_apply

added theorem Matrix.lieConj_symm_apply

added def Matrix.reindexLieEquiv

added theorem Matrix.reindexLieEquiv_apply

added theorem Matrix.reindexLieEquiv_symm

added def lieEquivMatrix'

added theorem lieEquivMatrix'_apply

added theorem lieEquivMatrix'_symm_apply