Definition of scaling of additive Haar measure

[kbuzzard]

The file HaarMeasure/ModularCharacter.lean defines the "modular character" https://math.stackexchange.com/questions/2237765/how-is-the-modular-character-usually-defined of a locally compact Hausdorff topological group; it's the factor which left Haar measure is scaled by under right multiplication.

In FLT we need a variant of this. Let R be a locally compact topological ring (possibly commutative). An element u of the units R^x of R induces (via multiplication) a homeomorphism R -> R which is also an isomorphism of additive groups, and hence scales additive Haar measure on R by some factor. We need a definition of this; the sorry'd definition is in the file HaarMeasure/Map.lean.

[morrison-daniel]

claim

[kbuzzard]

@morrison-daniel this might have been done last week by Yael Dillies in #223 .

[morrison-daniel]

unclaim

[morrison-daniel]

disclaim

[kbuzzard]

@YaelDillies can you claim this, given that you've essentially done it? I think all we need is a namechange?

[YaelDillies]

claim

[YaelDillies]

propose #263