[Merged by Bors] - feat(linear_algebra/bilinear_form): add is_refl and ortho_sym for alt_bilin_form #10304
Conversation
…_bilin_form 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.
There was a problem hiding this comment.
I think the API for sym_bilin_form / alt_bilin_form / refl_bilin_form is in need of a cleanup, but this change looks like it fits the existing pattern so that cleanup makes sense to leave for another PR.
That cleanup in my mind would be to rename sym_bilin_form.is_sym to bilin_form.is_symm, alt_bilin_form.is_alt to bilin_form.is_alt, etc, if you're interested in making another small PR after this one is merged.
bors d+
|
✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with |
eric-wieser
added
the
awaiting-CI
github-actions
bot
added
the
delegated
| end | ||
|
|
||
| lemma ortho_sym (H : is_alt B₁) {x y : M₁} : | ||
| is_ortho B₁ x y ↔ is_ortho B₁ y x := refl_bilin_form.ortho_sym (is_refl H) |
There was a problem hiding this comment.
Note if we made the rename I suggest in another PR, this will become the shorter
is_ortho B₁ x y ↔ is_ortho B₁ y x := H.is_refl.ortho_sym Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
github-actions
bot
removed
the
awaiting-CI
|
bors r+ |
…_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.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Lemma
is_reflshows that every alternating bilinear form is reflexive.Lemma
ortho_symshows that being orthogonal with respect to an alternating bilinear form is symmetric.