Commit 2022-05-24 10:24 65f1f8e2
View on Github →feat(linear_algebra/quadratic_form/isometry): extract from linear_algebra/quadratic_form/basic (#14305)
150 lines seems worthy of its own file, especially if this grows fun_like boilerplate in future.
No lemmas have been renamed or proofs changed.