mathlib3

65f1f8e2 - feat(linear_algebra/quadratic_form/isometry): extract from `linear_algebra/quadratic_form/basic` (#14305)

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.