Mathlib v3 is deprecated. Go to Mathlib v4

Def quadratic_form.isometry_of_comp_linear_equiv

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.isometry_of_comp_linear_equivView on Github →
2021-06-07 15:40
src/linear_algebra/quadratic_form.lean
feat(linear_algebra/quadratic_form): Complex version of Sylvester's law of inertia (#7416) …
Added quadratic_form.isometry_of_comp_linear_equivView on Github →