mathlib3
fa371f7b - feat(linear_algebra/bilinear_form): introduce adjoints of linear maps (#2746)

Commit
5 years ago
feat(linear_algebra/bilinear_form): introduce adjoints of linear maps (#2746) We also use this to define the Lie algebra structure on skew-adjoint endomorphisms / matrices. The motivation is to enable us to define the classical Lie algebras.
Author
Oliver Nash
Parents
Loading