Commit 2021-11-13 09:09 a7e38a03
View on Github →feat(linear_algebra/bilinear_form): add is_refl and ortho_sym for alt_bilin_form (#10304)
Lemma is_refl shows that every alternating bilinear form is reflexive.
Lemma ortho_sym shows that being orthogonal with respect to an alternating bilinear form is symmetric.