Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-24 09:15 fe4abe00

View on Github →

chore(algebra/lie/skew_adjoint): move logic for Lie algebras of skew-adjoint endomorphisms to own file (#5098)

Estimated changes

Modified src/algebra/lie/basic.lean

deleted theorem bilin_form.is_skew_adjoint_bracket

deleted theorem matrix.is_skew_adjoint_bracket

deleted theorem matrix.lie_transpose

deleted theorem mem_skew_adjoint_matrices_lie_subalgebra

deleted theorem mem_skew_adjoint_matrices_lie_subalgebra_unit_smul

deleted def skew_adjoint_lie_subalgebra

deleted def skew_adjoint_lie_subalgebra_equiv

deleted theorem skew_adjoint_lie_subalgebra_equiv_apply

deleted theorem skew_adjoint_lie_subalgebra_equiv_symm_apply

deleted def skew_adjoint_matrices_lie_subalgebra

deleted theorem skew_adjoint_matrices_lie_subalgebra_equiv_apply

deleted def skew_adjoint_matrices_lie_subalgebra_equiv_transpose

deleted theorem skew_adjoint_matrices_lie_subalgebra_equiv_transpose_apply

Modified src/algebra/lie/classical.lean

Created src/algebra/lie/skew_adjoint.lean

added theorem bilin_form.is_skew_adjoint_bracket

added theorem matrix.is_skew_adjoint_bracket

added theorem matrix.lie_transpose

added theorem mem_skew_adjoint_matrices_lie_subalgebra

added theorem mem_skew_adjoint_matrices_lie_subalgebra_unit_smul

added def skew_adjoint_lie_subalgebra

added def skew_adjoint_lie_subalgebra_equiv

added theorem skew_adjoint_lie_subalgebra_equiv_apply

added theorem skew_adjoint_lie_subalgebra_equiv_symm_apply

added def skew_adjoint_matrices_lie_subalgebra

added theorem skew_adjoint_matrices_lie_subalgebra_equiv_apply

added def skew_adjoint_matrices_lie_subalgebra_equiv_transpose

added theorem skew_adjoint_matrices_lie_subalgebra_equiv_transpose_apply