Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quadratic_form.equivalent.symm

Modification history

2022-05-24 10:24
src/linear_algebra/quadratic_form/basic.lean
feat(linear_algebra/quadratic_form/isometry): extract from `linear_algebra/quadratic_form/basic` (#14305) …
Modified quadratic_form.equivalent.symmView on Github →
2020-05-26 16:47
src/linear_algebra/quadratic_form.lean
feat(linear_algebra/quadratic_form): equivalence of quadratic forms (#2769)
Added quadratic_form.equivalent.symmView on Github →