Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 17:14 b3915636

View on Github →

feat(algebra/lie_algebra): conjugation transformation for Lie algebras of skew-adjoint endomorphims, matrices (#3229) The two main results are the lemmas:

  • skew_adjoint_lie_subalgebra_equiv
  • skew_adjoint_matrices_lie_subalgebra_equiv The latter is expected to be useful when defining the classical Lie algebras of type B and D.

Estimated changes

added theorem lie_subalgebra.ext
added theorem lie_subalgebra.ext_iff
modified def lie_subalgebra.incl
added theorem lie_subalgebra.mem_coe
added theorem matrix.lie_conj_apply
added theorem matrix.lie_transpose
added theorem matrix.transpose_sub
modified theorem linear_equiv.conj_apply
added theorem linear_equiv.conj_comp
modified theorem matrix.diagonal_to_lin
modified theorem matrix.proj_diagonal