forked from leanprover-community/mathlib4
-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Labels
help wantedExtra attention is neededExtra attention is needed
Description
Define Skew-symmetric and skew-Hermitian matrices, and prove cool properties from their Wikipedia pages.
These are also called anti-symmetric / anti-Hermitian, maybe do a literature search to see what's more common.
Maybe also link it to StarModule.selfAdjointPart_add_skewAdjointPart to show that every matrix is the sum of a Hermitian matrix and a skew-Hermitian matrix.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
help wantedExtra attention is neededExtra attention is needed