mathlib3
a7e38a03 - feat(linear_algebra/bilinear_form): add is_refl and ortho_sym for alt_bilin_form (#10304)

Commit
4 years ago
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.
Author
Parents
Loading