Commit 2023-02-01 12:38 11b92770

View on Github →

feat(linear_algebra/bilinear_form): arithmetic lemmas about symm/refl/alt (#18340) The only vaguelly non-trivial result here is bilin_form.is_refl.smul, the rest follow essentially by definition.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

deleted theorem bilin_form.is_alt.neg

added theorem bilin_form.is_alt.neg_eq

added theorem bilin_form.is_alt_neg

added theorem bilin_form.is_alt_zero

added theorem bilin_form.is_refl_neg

added theorem bilin_form.is_refl_zero

added theorem bilin_form.is_symm_neg

added theorem bilin_form.is_symm_zero

Modified src/linear_algebra/quadratic_form/basic.lean

added theorem bilin_form.to_quadratic_form_eq_zero