Commit 2023-06-07 10:11 468830c8

View on Github →

feat: port Algebra.Lie.Classical (#4788)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Invertible.lean

Created Mathlib/Algebra/Lie/Classical.lean

added def LieAlgebra.Orthogonal.JB

added def LieAlgebra.Orthogonal.JD

added def LieAlgebra.Orthogonal.PB

added def LieAlgebra.Orthogonal.PD

added def LieAlgebra.Orthogonal.Pso

added def LieAlgebra.Orthogonal.S

added def LieAlgebra.Orthogonal.indefiniteDiagonal

added theorem LieAlgebra.Orthogonal.indefiniteDiagonal_assoc

added theorem LieAlgebra.Orthogonal.indefiniteDiagonal_transform

added def LieAlgebra.Orthogonal.invertiblePso

added theorem LieAlgebra.Orthogonal.jb_transform

added theorem LieAlgebra.Orthogonal.jd_transform

added theorem LieAlgebra.Orthogonal.mem_so

added theorem LieAlgebra.Orthogonal.pb_inv

added theorem LieAlgebra.Orthogonal.pd_inv

added theorem LieAlgebra.Orthogonal.pso_inv

added theorem LieAlgebra.Orthogonal.s_as_blocks

added def LieAlgebra.Orthogonal.so'

added def LieAlgebra.Orthogonal.so

added def LieAlgebra.Orthogonal.soIndefiniteEquiv

added theorem LieAlgebra.Orthogonal.soIndefiniteEquiv_apply

added def LieAlgebra.Orthogonal.typeB

added def LieAlgebra.Orthogonal.typeBEquivSo'

added def LieAlgebra.Orthogonal.typeD

added def LieAlgebra.Orthogonal.typeDEquivSo'

added def LieAlgebra.SpecialLinear.Eb

added theorem LieAlgebra.SpecialLinear.eb_val

added def LieAlgebra.SpecialLinear.sl

added theorem LieAlgebra.SpecialLinear.sl_bracket

added theorem LieAlgebra.SpecialLinear.sl_non_abelian

added def LieAlgebra.Symplectic.sp

added theorem LieAlgebra.matrix_trace_commutator_zero