Commit 2020-08-05 10:42 0531cb0c

View on Github →

feat(algebra/classical_lie_algebras): add definitions of missing classical Lie algebras (#3661) Copying from the comments I have added at the top of classical_lie_algebras.lean:

Main definitions

lie_algebra.symplectic.sp
lie_algebra.orthogonal.so
lie_algebra.orthogonal.so'
lie_algebra.orthogonal.so_indefinite_equiv
lie_algebra.orthogonal.type_D
lie_algebra.orthogonal.type_B
lie_algebra.orthogonal.type_D_equiv_so'
lie_algebra.orthogonal.type_B_equiv_so'

Estimated changes

Modified src/algebra/classical_lie_algebras.lean

added def lie_algebra.orthogonal.JB

added theorem lie_algebra.orthogonal.JB_transform

added def lie_algebra.orthogonal.JD

added theorem lie_algebra.orthogonal.JD_transform

added def lie_algebra.orthogonal.PB

added theorem lie_algebra.orthogonal.PB_inv

added def lie_algebra.orthogonal.PD

added theorem lie_algebra.orthogonal.PD_inv

added def lie_algebra.orthogonal.Pso

added theorem lie_algebra.orthogonal.Pso_inv

added def lie_algebra.orthogonal.S

added theorem lie_algebra.orthogonal.S_as_blocks

added def lie_algebra.orthogonal.indefinite_diagonal

added theorem lie_algebra.orthogonal.indefinite_diagonal_assoc

added theorem lie_algebra.orthogonal.indefinite_diagonal_transform

added theorem lie_algebra.orthogonal.is_unit_PB

added theorem lie_algebra.orthogonal.is_unit_PD

added theorem lie_algebra.orthogonal.is_unit_Pso

added def lie_algebra.orthogonal.so'

added def lie_algebra.orthogonal.so

added theorem lie_algebra.orthogonal.so_indefinite_equiv_apply

added def lie_algebra.orthogonal.type_B

added def lie_algebra.orthogonal.type_D

added def lie_algebra.symplectic.J

added def lie_algebra.symplectic.sp

Modified src/algebra/lie_algebra.lean

added def alg_equiv.to_lie_equiv

added theorem alg_equiv.to_lie_equiv_apply

added theorem alg_equiv.to_lie_equiv_symm_apply

added theorem mem_skew_adjoint_matrices_lie_subalgebra

added theorem mem_skew_adjoint_matrices_lie_subalgebra_unit_smul

added def skew_adjoint_matrices_lie_subalgebra_equiv_transpose

added theorem skew_adjoint_matrices_lie_subalgebra_equiv_transpose_apply

Modified src/data/matrix/basic.lean

added def matrix.from_blocks

added theorem matrix.from_blocks_add

added theorem matrix.from_blocks_apply₁₁

added theorem matrix.from_blocks_apply₁₂

added theorem matrix.from_blocks_apply₂₁

added theorem matrix.from_blocks_apply₂₂

added theorem matrix.from_blocks_diagonal

added theorem matrix.from_blocks_multiply

added theorem matrix.from_blocks_one

added theorem matrix.from_blocks_smul

added theorem matrix.from_blocks_to_blocks

added theorem matrix.from_blocks_transpose

added theorem matrix.to_blocks_from_blocks₁₁

added theorem matrix.to_blocks_from_blocks₁₂

added theorem matrix.to_blocks_from_blocks₂₁

added theorem matrix.to_blocks_from_blocks₂₂

added def matrix.to_blocks₁₁

added def matrix.to_blocks₁₂

added def matrix.to_blocks₂₁

added def matrix.to_blocks₂₂

Modified src/linear_algebra/matrix.lean

added theorem matrix.reindex_transpose

Modified src/linear_algebra/nonsingular_inverse.lean

added theorem matrix.is_unit_det_of_left_inverse

added theorem matrix.is_unit_det_of_right_inverse

added theorem matrix.nonsing_inv_left_right

added theorem matrix.nonsing_inv_right_left

Modified src/ring_theory/algebra.lean

added def alg_equiv.to_linear_equiv

added theorem alg_equiv.to_linear_equiv_apply