Given φ : G ≃ₜ* G and ψ : H ≃ₜ* H, fudge factor for φ.prodCongr ψ is product of fudge factors

[kbuzzard]

We don't need second countable here, thanks to an argument of Gouezel. See the argument in the blueprint. This is MeasureTheory.mulEquivHaarChar_prodCongr in FLT/HaarMeasure/HaarChar/AddEquiv.lean.

[Ruben-VandeVelde]

https://imperialcollegelondon.github.io/FLT/blueprint/Haar_char_project.html#MeasureTheory.addEquivAddHaarChar_prodCongr

[js2357]

#566 is addressing what I think might be an issue not mentioned in the blueprint's proof. But if anyone else wants to claim this task, feel free to take it.

[kbuzzard]

https://imperialcollegelondon.github.io/FLT/blueprint/Haar_char_project.html#MeasureTheory.addEquivAddHaarChar_prodCongr

Thanks!

The practical problem I'm having here is that I tend to open the issues and mark them WIP while I'm in the process of writing the LaTeX/Lean (so I can include the issue number in the Lean code and LaTeX) and at that point the URL I'd like to include doesn't work because the PR isn't merged yet.