Add Equiv Add Haar Char eq ring Haar Char det pi

lemma addEquivAddHaarChar_eq_ringHaarChar_det_pi [SecondCountableTopology F]    (ρ : (ι → F) ≃L[F] (ι → F))    (hρM : Pivot.ExistsListTransvecMulDiagonalMulListTransvec      (ρ.toLinearEquiv.toMatrix (Pi.basisFun F ι) (Pi.basisFun F ι))) :    addEquivAddHaarChar ρ.toContinuousAddEquiv = ringHaarChar ρ.toLinearEquiv.det := by  classical  let e := ρ.toLinearEquiv  let b := Pi.basisFun F ι  let M := e.toMatrix b b  have hM : IsUnit M.det := by simp [M, e, LinearEquiv.isUnit_det']  -- identify ρ with the matrix-induced equivalence  have hρ : ρ = (M.toContinuousLinearEquiv b hM) :=    (ContinuousLinearEquiv.toMatrix_toContinousLinearEquiv b ρ).symm  rw [hρ]  exact addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi M hρM hM