mathlib

11b92770 - feat(linear_algebra/bilinear_form): arithmetic lemmas about symm/refl/alt (#18340)

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.