Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-28 07:50 fa371f7b

View on Github →

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.

Estimated changes

added theorem bilin_form.neg_apply