Add Equiv Add Haar Char eq ring Haar Char det of exists List Transvec Etc

theorem addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc    [SecondCountableTopology F] (ρ : V ≃L[F] V) (n : ℕ) (b : Basis (Fin n) F V)    (hρ : Pivot.ExistsListTransvecMulDiagonalMulListTransvec      (ρ.toLinearMap.toMatrix b b)) :    addEquivAddHaarChar ρ.toContinuousAddEquiv = ringHaarChar ρ.toLinearEquiv.det := by  let ι := Fin n  let e : V ≃ₗ[F] ι → F := Basis.equivFun b  have he : Continuous e := IsModuleTopology.continuous_of_linearMap e.toLinearMap  have he_inv : Continuous e.symm := IsModuleTopology.continuous_of_linearMap e.symm.toLinearMap  let ec : V ≃L[F] (ι → F) := ⟨e, he, he_inv⟩  let f := ec.toContinuousAddEquiv  let ρ' : (ι → F) ≃ₜ+ (ι → F) := (f.symm.trans (ρ.toContinuousAddEquiv)).trans f  have hComm: ∀ x, f (ρ.toContinuousAddEquiv x) = ρ' (f x) := by    simp [f, ρ', ContinuousAddEquiv.trans_apply, ContinuousAddEquiv.eq_symm_apply]  let h_eq := addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv f    ρ.toContinuousAddEquiv ρ' hComm  have : (ec.toContinuousAddEquiv.symm.trans      ρ.toContinuousAddEquiv).trans ec.toContinuousAddEquiv =      ((ec.symm.trans ρ).trans ec).toContinuousAddEquiv := rfl  have this₂ := addEquivAddHaarChar_eq_ringHaarChar_det_pi (((ec.symm.trans ρ).trans ec))    hρ  simp [h_eq, ρ', f, this, this₂]