Mathlib v3 is deprecated. Go to Mathlib v4

Structure quadratic_form.isometry

Modification history

2022-07-30 06:36
src/linear_algebra/quadratic_form/isometry.lean
refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542) …
Modified quadratic_form.isometryView on Github →
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.isometryView 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.isometryView on Github →