English
For continuous multiplicative equivalences φ, ψ, mulEquivHaarChar(ψ.trans φ) = mulEquivHaarChar ψ · mulEquivHaarChar φ.
Русский
Для отображений φ, ψ: mulEquivHaarChar(ψ.trans φ) = mulEquivHaarChar ψ · mulEquivHaarChar φ.
LaTeX
$$$mulEquivHaarChar(\psi. trans \phi) = mulEquivHaarChar(\psi) \cdot mulEquivHaarChar(\phi)$$$
Lean4
@[to_additive]
theorem mulEquivHaarChar_trans {φ ψ : G ≃ₜ* G} :
mulEquivHaarChar (ψ.trans φ) = mulEquivHaarChar ψ * mulEquivHaarChar φ :=
by
rw [mulEquivHaarChar_eq haar ψ, mulEquivHaarChar_eq haar (ψ.trans φ)]
have hφ : Measurable φ := by fun_prop
have hψ : Measurable ψ := by fun_prop
simp_rw [ContinuousMulEquiv.coe_trans, ← map_map hφ hψ]
have h_reg : (haar.map ψ).Regular := Regular.map ψ.toHomeomorph
rw [MeasureTheory.Measure.haarScalarFactor_eq_mul haar (haar.map ψ), ← mulEquivHaarChar_eq (haar.map ψ)]
