From e7fe6ca18b9bd24f82abca4a6c501f9f1fdafc91 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 17 Jul 2023 21:13:31 +0000 Subject: [PATCH] another trivial definition --- .../linear_algebra/quadratic_form/isometric_map.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean index 7ab88791f..172dd8608 100644 --- a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean +++ b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean @@ -58,8 +58,14 @@ def comp (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) : Q₁.isom map_app' := by { intro m, rw [← f.map_app, ← g.map_app] }, .. (g.to_linear_map : M₂ →ₗ[R] M₃).comp (f.to_linear_map : M₁ →ₗ[R] M₂) } -@[simp] lemma to_linear_map_comp (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) : +@[simp] lemma to_linear_map_comp (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) : (g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl +/-- Isometries are isometric maps -/ +@[simps?] +def _root_.quadratic_form.isometry.to_isometric_map (g : Q₁.isometry Q₂) : + Q₁.isometric_map Q₂ := { ..g } + end isometric_map + end quadratic_form