mathlib
2ff12ea3 - feat(linear_algebra/bilinear_form): generalize from is_symm to is_refl (#13181)

Commit
3 years ago
feat(linear_algebra/bilinear_form): generalize from is_symm to is_refl (#13181) Generalize some lemmas that assumed symmetric bilinear forms to reflexive bilinear forms (which is more general) and update docstring (before the condition 'symmetric' was not mentioned) Co-authored-by: tinval <44555630+tinval@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
tinval
Parents
Loading