refactor(LinearAlgebra/QuadraticForm): rename Isometry to `Isometry…

…Equiv` (#6305)

This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism.

Mathlib.lean

@@ -2227,7 +2227,7 @@ import Mathlib.LinearAlgebra.ProjectiveSpace.Independence
 import Mathlib.LinearAlgebra.ProjectiveSpace.Subspace
 import Mathlib.LinearAlgebra.QuadraticForm.Basic
 import Mathlib.LinearAlgebra.QuadraticForm.Complex
-import Mathlib.LinearAlgebra.QuadraticForm.Isometry
+import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
 import Mathlib.LinearAlgebra.QuadraticForm.Prod
 import Mathlib.LinearAlgebra.QuadraticForm.Real
 import Mathlib.LinearAlgebra.Quotient

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -5,7 +5,7 @@ Authors: Eric Wieser, Utensil Song
 -/
 import Mathlib.Algebra.RingQuot
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
-import Mathlib.LinearAlgebra.QuadraticForm.Isometry
+import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
 
 #align_import linear_algebra.clifford_algebra.basic from "leanprover-community/mathlib"@"d46774d43797f5d1f507a63a6e904f7a533ae74a"
 
@@ -315,7 +315,7 @@ variable {Q₁ Q₂ Q₃}
 /-- Two `CliffordAlgebra`s are equivalent as algebras if their quadratic forms are
 equivalent. -/
 @[simps! apply]
-def equivOfIsometry (e : Q₁.Isometry Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂ :=
+def equivOfIsometry (e : Q₁.IsometryEquiv Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂ :=
   AlgEquiv.ofAlgHom (map Q₁ Q₂ e e.map_app) (map Q₂ Q₁ e.symm e.symm.map_app)
     ((map_comp_map _ _ _ _ _ _ _).trans <| by
       convert map_id Q₂ using 2  -- porting note: replaced `_` with `Q₂`
@@ -328,21 +328,21 @@ def equivOfIsometry (e : Q₁.Isometry Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] Cl
 #align clifford_algebra.equiv_of_isometry CliffordAlgebra.equivOfIsometry
 
 @[simp]
-theorem equivOfIsometry_symm (e : Q₁.Isometry Q₂) :
+theorem equivOfIsometry_symm (e : Q₁.IsometryEquiv Q₂) :
     (equivOfIsometry e).symm = equivOfIsometry e.symm :=
   rfl
 #align clifford_algebra.equiv_of_isometry_symm CliffordAlgebra.equivOfIsometry_symm
 
 @[simp]
-theorem equivOfIsometry_trans (e₁₂ : Q₁.Isometry Q₂) (e₂₃ : Q₂.Isometry Q₃) :
+theorem equivOfIsometry_trans (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) :
     (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃) := by
   ext x
   exact AlgHom.congr_fun (map_comp_map Q₁ Q₂ Q₃ _ _ _ _) x
 #align clifford_algebra.equiv_of_isometry_trans CliffordAlgebra.equivOfIsometry_trans
 
 @[simp]
 theorem equivOfIsometry_refl :
-    (equivOfIsometry <| QuadraticForm.Isometry.refl Q₁) = AlgEquiv.refl := by
+    (equivOfIsometry <| QuadraticForm.IsometryEquiv.refl Q₁) = AlgEquiv.refl := by
   ext x
   exact AlgHom.congr_fun (map_id Q₁) x
 #align clifford_algebra.equiv_of_isometry_refl CliffordAlgebra.equivOfIsometry_refl

Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Kexing Ying, Eric Wieser
 -/
-import Mathlib.LinearAlgebra.QuadraticForm.Isometry
+import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
 
 #align_import linear_algebra.quadratic_form.complex from "leanprover-community/mathlib"@"0b9eaaa7686280fad8cce467f5c3c57ee6ce77f8"
@@ -27,14 +27,14 @@ variable {ι : Type _} [Fintype ι]
 
 /-- The isometry between a weighted sum of squares on the complex numbers and the
 sum of squares, i.e. `weightedSumSquares` with weights 1 or 0. -/
-noncomputable def isometrySumSquares [DecidableEq ι] (w' : ι → ℂ) :
-    Isometry (weightedSumSquares ℂ w')
+noncomputable def isometryEquivSumSquares [DecidableEq ι] (w' : ι → ℂ) :
+    IsometryEquiv (weightedSumSquares ℂ w')
       (weightedSumSquares ℂ (fun i => if w' i = 0 then 0 else 1 : ι → ℂ)) := by
   let w i := if h : w' i = 0 then (1 : Units ℂ) else Units.mk0 (w' i) h
   have hw' : ∀ i : ι, (w i : ℂ) ^ (-(1 / 2 : ℂ)) ≠ 0 := by
     intro i hi
     exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
-  convert (weightedSumSquares ℂ w').isometryBasisRepr
+  convert (weightedSumSquares ℂ w').isometryEquivBasisRepr
     ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit)
   ext1 v
   erw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]
@@ -60,22 +60,22 @@ noncomputable def isometrySumSquares [DecidableEq ι] (w' : ι → ℂ) :
     rw [this]; ring
   rw [← Complex.cpow_add _ _ (w j).ne_zero, show -(1 / 2 : ℂ) + -(1 / 2) = -1 by simp [← two_mul],
     Complex.cpow_neg_one, inv_mul_cancel (w j).ne_zero, one_mul]
-#align quadratic_form.isometry_sum_squares QuadraticForm.isometrySumSquares
+#align quadratic_form.isometry_sum_squares QuadraticForm.isometryEquivSumSquares
 
 /-- The isometry between a weighted sum of squares on the complex numbers and the
 sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/
-noncomputable def isometrySumSquaresUnits [DecidableEq ι] (w : ι → Units ℂ) :
-    Isometry (weightedSumSquares ℂ w) (weightedSumSquares ℂ (1 : ι → ℂ)) := by
-  simpa using isometrySumSquares ((↑) ∘ w)
-#align quadratic_form.isometry_sum_squares_units QuadraticForm.isometrySumSquaresUnits
+noncomputable def isometryEquivSumSquaresUnits [DecidableEq ι] (w : ι → Units ℂ) :
+    IsometryEquiv (weightedSumSquares ℂ w) (weightedSumSquares ℂ (1 : ι → ℂ)) := by
+  simpa using isometryEquivSumSquares ((↑) ∘ w)
+#align quadratic_form.isometry_sum_squares_units QuadraticForm.isometryEquivSumSquaresUnits
 
 /-- A nondegenerate quadratic form on the complex numbers is equivalent to
 the sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/
 theorem equivalent_sum_squares {M : Type _} [AddCommGroup M] [Module ℂ M] [FiniteDimensional ℂ M]
     (Q : QuadraticForm ℂ M) (hQ : (associated (R₁ := ℂ) Q).Nondegenerate) :
     Equivalent Q (weightedSumSquares ℂ (1 : Fin (FiniteDimensional.finrank ℂ M) → ℂ)) :=
   let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
-  ⟨hw₁.trans (isometrySumSquaresUnits w)⟩
+  ⟨hw₁.trans (isometryEquivSumSquaresUnits w)⟩
 #align quadratic_form.equivalent_sum_squares QuadraticForm.equivalent_sum_squares
 
 /-- All nondegenerate quadratic forms on the complex numbers are equivalent. -/

Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean → Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

@@ -8,11 +8,11 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic
 #align_import linear_algebra.quadratic_form.isometry from "leanprover-community/mathlib"@"14b69e9f3c16630440a2cbd46f1ddad0d561dee7"
 
 /-!
-# Isometries with respect to quadratic forms
+# Isometric equivalences with respect to quadratic forms
 
 ## Main definitions
 
-* `QuadraticForm.Isometry`: `LinearEquiv`s which map between two different quadratic forms
+* `QuadraticForm.IsometryEquiv`: `LinearEquiv`s which map between two different quadratic forms
 * `QuadraticForm.Equivalent`: propositional version of the above
 
 ## Main results
@@ -32,78 +32,79 @@ variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMon
 
 variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃]
 
-/-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
+/-- An isometric equivalence between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
 is a linear equivalence between `M₁` and `M₂` that commutes with the quadratic forms. -/
 -- Porting note: not implemented @[nolint has_nonempty_instance]
-structure Isometry (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) extends M₁ ≃ₗ[R] M₂ where
+structure IsometryEquiv (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
+    extends M₁ ≃ₗ[R] M₂ where
   map_app' : ∀ m, Q₂ (toFun m) = Q₁ m
-#align quadratic_form.isometry QuadraticForm.Isometry
+#align quadratic_form.isometry QuadraticForm.IsometryEquiv
 
 /-- Two quadratic forms over a ring `R` are equivalent
-if there exists an isometry between them:
+if there exists an isometric equivalence between them:
 a linear equivalence that transforms one quadratic form into the other. -/
-def Equivalent (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :=
-  Nonempty (Q₁.Isometry Q₂)
+def Equivalent (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Prop :=
+  Nonempty (Q₁.IsometryEquiv Q₂)
 #align quadratic_form.equivalent QuadraticForm.Equivalent
 
-namespace Isometry
+namespace IsometryEquiv
 
 variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
 
 -- Porting note: was `Coe`
-instance : CoeOut (Q₁.Isometry Q₂) (M₁ ≃ₗ[R] M₂) :=
-  ⟨Isometry.toLinearEquiv⟩
+instance : CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂) :=
+  ⟨IsometryEquiv.toLinearEquiv⟩
 
 -- Porting note: syntaut
 #noalign quadratic_form.isometry.to_linear_equiv_eq_coe
 
 --Porting note: replace `CoeFun` with `EquivLike`
-instance : EquivLike (Q₁.Isometry Q₂) M₁ M₂ :=
+instance : EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂ :=
   { coe := fun f => ⇑(f : M₁ ≃ₗ[R] M₂),
     inv := fun f => ⇑(f : M₁ ≃ₗ[R] M₂).symm,
     left_inv := fun f => (f : M₁ ≃ₗ[R] M₂).left_inv
     right_inv := fun f => (f : M₁ ≃ₗ[R] M₂).right_inv
     coe_injective' := fun f g => by cases f; cases g; simp (config := {contextual := true}) }
 
 @[simp]
-theorem coe_toLinearEquiv (f : Q₁.Isometry Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f :=
+theorem coe_toLinearEquiv (f : Q₁.IsometryEquiv Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f :=
   rfl
-#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.Isometry.coe_toLinearEquiv
+#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.IsometryEquiv.coe_toLinearEquiv
 
 @[simp]
-theorem map_app (f : Q₁.Isometry Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
+theorem map_app (f : Q₁.IsometryEquiv Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
   f.map_app' m
-#align quadratic_form.isometry.map_app QuadraticForm.Isometry.map_app
+#align quadratic_form.isometry.map_app QuadraticForm.IsometryEquiv.map_app
 
-/-- The identity isometry from a quadratic form to itself. -/
+/-- The identity isometric equivalence between a quadratic form and itself. -/
 @[refl]
-def refl (Q : QuadraticForm R M) : Q.Isometry Q :=
+def refl (Q : QuadraticForm R M) : Q.IsometryEquiv Q :=
   { LinearEquiv.refl R M with map_app' := fun _ => rfl }
-#align quadratic_form.isometry.refl QuadraticForm.Isometry.refl
+#align quadratic_form.isometry.refl QuadraticForm.IsometryEquiv.refl
 
-/-- The inverse isometry of an isometry between two quadratic forms. -/
+/-- The inverse isometric equivalence of an isometric equivalence between two quadratic forms. -/
 @[symm]
-def symm (f : Q₁.Isometry Q₂) : Q₂.Isometry Q₁ :=
+def symm (f : Q₁.IsometryEquiv Q₂) : Q₂.IsometryEquiv Q₁ :=
   { (f : M₁ ≃ₗ[R] M₂).symm with
     map_app' := by intro m; rw [← f.map_app]; congr; exact f.toLinearEquiv.apply_symm_apply m }
-#align quadratic_form.isometry.symm QuadraticForm.Isometry.symm
+#align quadratic_form.isometry.symm QuadraticForm.IsometryEquiv.symm
 
-/-- The composition of two isometries between quadratic forms. -/
+/-- The composition of two isometric equivalences between quadratic forms. -/
 @[trans]
-def trans (f : Q₁.Isometry Q₂) (g : Q₂.Isometry Q₃) : Q₁.Isometry Q₃ :=
+def trans (f : Q₁.IsometryEquiv Q₂) (g : Q₂.IsometryEquiv Q₃) : Q₁.IsometryEquiv Q₃ :=
   { (f : M₁ ≃ₗ[R] M₂).trans (g : M₂ ≃ₗ[R] M₃) with
     map_app' := by intro m; rw [← f.map_app, ← g.map_app]; rfl }
-#align quadratic_form.isometry.trans QuadraticForm.Isometry.trans
+#align quadratic_form.isometry.trans QuadraticForm.IsometryEquiv.trans
 
-end Isometry
+end IsometryEquiv
 
 namespace Equivalent
 
 variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
 
 @[refl]
 theorem refl (Q : QuadraticForm R M) : Q.Equivalent Q :=
-  ⟨Isometry.refl Q⟩
+  ⟨IsometryEquiv.refl Q⟩
 #align quadratic_form.equivalent.refl QuadraticForm.Equivalent.refl
 
 @[symm]
@@ -121,33 +122,34 @@ end Equivalent
 variable [Fintype ι] {v : Basis ι R M}
 
 /-- A quadratic form composed with a `LinearEquiv` is isometric to itself. -/
-def isometryOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) :
-    Q.Isometry (Q.comp (f : M₁ →ₗ[R] M)) :=
+def isometryEquivOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) :
+    Q.IsometryEquiv (Q.comp (f : M₁ →ₗ[R] M)) :=
   { f.symm with
     map_app' := by
       intro
       simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
         LinearEquiv.apply_symm_apply, f.apply_symm_apply] }
-#align quadratic_form.isometry_of_comp_linear_equiv QuadraticForm.isometryOfCompLinearEquiv
+#align quadratic_form.isometry_of_comp_linear_equiv QuadraticForm.isometryEquivOfCompLinearEquiv
 
-/-- A quadratic form is isometric to its bases representations. -/
-noncomputable def isometryBasisRepr (Q : QuadraticForm R M) (v : Basis ι R M) :
-    Isometry Q (Q.basisRepr v) :=
-  isometryOfCompLinearEquiv Q v.equivFun.symm
-#align quadratic_form.isometry_basis_repr QuadraticForm.isometryBasisRepr
+/-- A quadratic form is isometrically equivalent to its bases representations. -/
+noncomputable def isometryEquivBasisRepr (Q : QuadraticForm R M) (v : Basis ι R M) :
+    IsometryEquiv Q (Q.basisRepr v) :=
+  isometryEquivOfCompLinearEquiv Q v.equivFun.symm
+#align quadratic_form.isometry_basis_repr QuadraticForm.isometryEquivBasisRepr
 
 variable [Field K] [Invertible (2 : K)] [AddCommGroup V] [Module K V]
 
-/-- Given an orthogonal basis, a quadratic form is isometric with a weighted sum of squares. -/
-noncomputable def isometryWeightedSumSquares (Q : QuadraticForm K V)
+/-- Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of
+squares. -/
+noncomputable def isometryEquivWeightedSumSquares (Q : QuadraticForm K V)
     (v : Basis (Fin (FiniteDimensional.finrank K V)) K V)
     (hv₁ : (associated (R₁ := K) Q).iIsOrtho v) :
-    Q.Isometry (weightedSumSquares K fun i => Q (v i)) := by
-  let iso := Q.isometryBasisRepr v
+    Q.IsometryEquiv (weightedSumSquares K fun i => Q (v i)) := by
+  let iso := Q.isometryEquivBasisRepr v
   refine' ⟨iso, fun m => _⟩
   convert iso.map_app m
   rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]
-#align quadratic_form.isometry_weighted_sum_squares QuadraticForm.isometryWeightedSumSquares
+#align quadratic_form.isometry_weighted_sum_squares QuadraticForm.isometryEquivWeightedSumSquares
 
 variable [FiniteDimensional K V]
 
@@ -156,7 +158,7 @@ open BilinForm
 theorem equivalent_weightedSumSquares (Q : QuadraticForm K V) :
     ∃ w : Fin (FiniteDimensional.finrank K V) → K, Equivalent Q (weightedSumSquares K w) :=
   let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm _ Q)
-  ⟨_, ⟨Q.isometryWeightedSumSquares v hv₁⟩⟩
+  ⟨_, ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩
 #align quadratic_form.equivalent_weighted_sum_squares QuadraticForm.equivalent_weightedSumSquares
 
 theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm K V)
@@ -165,7 +167,7 @@ theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm
   obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
   have hv₂ := hv₁.not_isOrtho_basis_self_of_nondegenerate hQ
   simp_rw [IsOrtho, associated_eq_self_apply] at hv₂
-  exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryWeightedSumSquares v hv₁⟩⟩
+  exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩
 #align quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate' QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'
 
 end QuadraticForm

Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.LinearAlgebra.QuadraticForm.Isometry
+import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
 
 #align_import linear_algebra.quadratic_form.prod from "leanprover-community/mathlib"@"9b2755b951bc323c962bd072cd447b375cf58101"
 
@@ -58,17 +58,19 @@ def prod (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Quadratic
 /-- An isometry between quadratic forms generated by `QuadraticForm.prod` can be constructed
 from a pair of isometries between the left and right parts. -/
 @[simps toLinearEquiv]
-def Isometry.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₁' : QuadraticForm R N₁}
-    {Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Isometry Q₁') (e₂ : Q₂.Isometry Q₂') :
-    (Q₁.prod Q₂).Isometry (Q₁'.prod Q₂') where
+def IsometryEquiv.prod
+    {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
+    {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂}
+    (e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') :
+    (Q₁.prod Q₂).IsometryEquiv (Q₁'.prod Q₂') where
   map_app' x := congr_arg₂ (· + ·) (e₁.map_app x.1) (e₂.map_app x.2)
   toLinearEquiv := LinearEquiv.prod e₁.toLinearEquiv e₂.toLinearEquiv
-#align quadratic_form.isometry.prod QuadraticForm.Isometry.prod
+#align quadratic_form.isometry.prod QuadraticForm.IsometryEquiv.prod
 
 theorem Equivalent.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
     {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Equivalent Q₁')
     (e₂ : Q₂.Equivalent Q₂') : (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂') :=
-  Nonempty.map2 Isometry.prod e₁ e₂
+  Nonempty.map2 IsometryEquiv.prod e₁ e₂
 #align quadratic_form.equivalent.prod QuadraticForm.Equivalent.prod
 
 /-- If a product is anisotropic then its components must be. The converse is not true. -/
@@ -132,18 +134,19 @@ theorem pi_apply [Fintype ι] (Q : ∀ i, QuadraticForm R (Mᵢ i)) (x : ∀ i,
 /-- An isometry between quadratic forms generated by `QuadraticForm.pi` can be constructed
 from a pair of isometries between the left and right parts. -/
 @[simps toLinearEquiv]
-def Isometry.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)} {Q' : ∀ i, QuadraticForm R (Nᵢ i)}
-    (e : ∀ i, (Q i).Isometry (Q' i)) : (pi Q).Isometry (pi Q') where
+def IsometryEquiv.pi [Fintype ι]
+    {Q : ∀ i, QuadraticForm R (Mᵢ i)} {Q' : ∀ i, QuadraticForm R (Nᵢ i)}
+    (e : ∀ i, (Q i).IsometryEquiv (Q' i)) : (pi Q).IsometryEquiv (pi Q') where
   map_app' x := by
     simp only [pi_apply, LinearEquiv.piCongrRight, LinearEquiv.toFun_eq_coe,
-      Isometry.coe_toLinearEquiv, Isometry.map_app]
+      IsometryEquiv.coe_toLinearEquiv, IsometryEquiv.map_app]
   toLinearEquiv := LinearEquiv.piCongrRight fun i => (e i : Mᵢ i ≃ₗ[R] Nᵢ i)
-#align quadratic_form.isometry.pi QuadraticForm.Isometry.pi
+#align quadratic_form.isometry.pi QuadraticForm.IsometryEquiv.pi
 
 theorem Equivalent.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)}
     {Q' : ∀ i, QuadraticForm R (Nᵢ i)} (e : ∀ i, (Q i).Equivalent (Q' i)) :
     (pi Q).Equivalent (pi Q') :=
-  ⟨Isometry.pi fun i => Classical.choice (e i)⟩
+  ⟨IsometryEquiv.pi fun i => Classical.choice (e i)⟩
 #align quadratic_form.equivalent.pi QuadraticForm.Equivalent.pi
 
 /-- If a family is anisotropic then its components must be. The converse is not true. -/