fix

Author: YaelDillies

Mathlib/NumberTheory/NumberField/Units/Regulator.lean

@@ -77,7 +77,7 @@ theorem abs_det_eq_abs_det (u : Fin (rank K) → (𝓞 K)ˣ)
   -- And `g` corresponds to the restriction of `f⁻¹` to `{w // w ≠ w₂}`
   let g : {w // w ≠ w₂} ≃ Fin (rank K) :=
     (Equiv.subtypeEquiv f.symm (fun _ ↦ by simp [f])).trans
-      (finSuccAboveEquiv (f.symm w₂)).toEquiv.symm
+      (finSuccAboveEquiv (f.symm w₂)).symm
   have h_col := congr_arg abs <| Matrix.det_permute (g.trans e₂.symm)
     (Matrix.of fun i w : {w // w ≠ w₂} ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log)
   rw [abs_mul, ← Int.cast_abs, Equiv.Perm.sign_abs, Int.cast_one, one_mul] at h_col