Commit 2023-02-02 14:06 8a035e9a

feat(counterexamples/quadratic_form): symmetric bilinear forms in char 2 do not always inject into quadratic forms (#18146)

added def B

added theorem B_apply

added theorem B_ne_zero

added theorem is_alt_B

added theorem is_symm_B

added theorem {u}