English
For a locally compact group G with Haar measure Haar and a continuous multiplicative equivalence φ : G ≃ₜ* G, mulEquivHaarChar φ is the nonnegative real factor by which φ scales Haar measures; equivalently, the pushforward of Haar by φ is mulEquivHaarChar φ times Haar: haar.map φ = mulEquivHaarChar φ · haar.
Русский
Для локально компактной группы G с мерой Хаара Haar и непрерывной мультипликативной эквивалентой φ : G ≃ₜ* G коэффициент mulEquivHaarChar φ — неотрицательное действительное число, на которое масштабируется мера Хаара под действием φ; то есть haar.map φ = mulEquivHaarChar φ · haar.
LaTeX
$$$ (haar.map \phi) = mulEquivHaarChar(\phi) \cdot haar $$$
Lean4
/-- If `φ : G ≃ₜ* G` then `mulEquivHaarChar φ` is the positive real factor by which
`φ` scales Haar measures on `G`. -/
@[to_additive /-- If `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`. -/
]
noncomputable def mulEquivHaarChar (φ : G ≃ₜ* G) : ℝ≥0 :=
haarScalarFactor haar (haar.map φ)
