mathlib3

6dfb24cf - feat(algebra/star/self_adjoint): define skew-adjoint elements of a star additive group (#12013)

feat(algebra/star/self_adjoint): define skew-adjoint elements of a star additive group (#12013) This defines the skew-adjoint elements of a star additive group, as the additive subgroup that satisfies `star x = -x`. The development is analogous to that of `self_adjoint`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>