def ContinuousAddEquiv.mulLeft {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] (r : Rˣ) : R ≃ₜ+ R

The additive homeomorphism from a topological ring to itself, induced by left multiplication by a unit.

@[simp]

theorem ContinuousAddEquiv.mulLeft_apply {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] (r : Rˣ) (x : R) : (mulLeft r) x = ↑r * x

def ContinuousAddEquiv.mulRight {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] (r : Rˣ) : R ≃ₜ+ R

The additive homeomorphism from a topological ring to itself, induced by right multiplication by a unit.

@[simp]

theorem ContinuousAddEquiv.mulRight_apply {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] (r : Rˣ) (x : R) : (mulRight r) x = x * ↑r

@[simp]

theorem ContinuousAddEquiv.preimage_mulLeft_smul {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] (r : Rˣ) (s : Set R) : ⇑(mulLeft r) ⁻¹' (r • s) = s

theorem MeasureTheory.ringHaarChar_continuous {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Continuous fun (u : Rˣ) => addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u)

noncomputable def MeasureTheory.ringHaarChar {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Rˣ →ₜ* NNReal

ringHaarChar : Rˣ →ₜ* ℝ≥0 is the function sending a unit of a locally compact topological ring R to the positive real factor which left multiplication by the unit scales additive Haar measure by.

theorem MeasureTheory.ringHaarChar_toFun {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (r : Rˣ) : ringHaarChar r = addEquivAddHaarChar (ContinuousAddEquiv.mulLeft r)

theorem MeasureTheory.ringHaarChar_apply {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (r : Rˣ) : ringHaarChar r = addEquivAddHaarChar (ContinuousAddEquiv.mulLeft r)

theorem MeasureTheory.ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] {S : Type u_2} [Ring S] [TopologicalSpace S] [IsTopologicalRing S] [LocallyCompactSpace S] [MeasurableSpace S] [BorelSpace S] (f : R ≃A[ℤ] S) (r : Rˣ) : ringHaarChar r = ringHaarChar ((Units.map f.toMulEquiv.toMonoidHom) r)

Transport ringHaarChar across a continuous ℤ-algebra equivalence (in place of continuous ring equivalences since we don't have them).

theorem MeasureTheory.ringHaarChar_mul_integral {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (μ : Measure R) [μ.IsAddHaarMeasure] [μ.Regular] {f : R → ℝ} (hf : Measurable f) (u : Rˣ) : ↑(ringHaarChar u) * ∫ (r : R), f (↑u * r) ∂μ = ∫ (a : R), f a ∂μ

theorem MeasureTheory.ringHaarChar_mul_volume {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (μ : Measure R) [μ.IsAddHaarMeasure] [μ.Regular] {X : Set R} (u : Rˣ) : μ (u • X) = ↑(ringHaarChar u) * μ X

theorem MeasureTheory.ringHaarChar_eq_of_measure_smul_eq_mul {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] {μ : Measure R} [μ.IsAddHaarMeasure] [μ.Regular] {s : Set R} (hs₀ : μ s ≠ 0) (hs : μ s ≠ ⊤) {r : NNReal} {u : Rˣ} (hμgs : μ (u • s) = ↑r * μ s) : ringHaarChar u = r

noncomputable def MeasureTheory.ringHaarChar_ker (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Subgroup Rˣ

The kernel of the ringHaarChar : Rˣ → ℝ≥0, namely the units of a locally compact topological ring such that left multiplication by them does not change additive Haar measure.

theorem MeasureTheory.mem_ringHaarChar_ker {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (x : Rˣ) : x ∈ ringHaarChar_ker R ↔ ringHaarChar x = 1

theorem MeasureTheory.ringHaarChar_prod {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] {S : Type u_2} [Ring S] [TopologicalSpace S] [IsTopologicalRing S] [LocallyCompactSpace S] [MeasurableSpace S] [BorelSpace S] (u : Rˣ) (v : Sˣ) [SecondCountableTopologyEither R S] : ringHaarChar (MulEquiv.prodUnits.symm (u, v)) = ringHaarChar u * ringHaarChar v

theorem MeasureTheory.ringHaarChar_prod' {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] {S : Type u_2} [Ring S] [TopologicalSpace S] [IsTopologicalRing S] [LocallyCompactSpace S] [MeasurableSpace S] [BorelSpace S] (uv : (R × S)ˣ) [SecondCountableTopologyEither R S] : ringHaarChar uv = ringHaarChar (MulEquiv.prodUnits uv).1 * ringHaarChar (MulEquiv.prodUnits uv).2

theorem MeasureTheory.ringHaarChar_pi {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] [Fintype ι] [∀ (i : ι), SecondCountableTopology (A i)] (u : (i : ι) → (A i)ˣ) : ringHaarChar (MulEquiv.piUnits.symm u) = ∏ i : ι, ringHaarChar (u i)

theorem MeasureTheory.ringHaarChar_pi' {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] [Fintype ι] [∀ (i : ι), SecondCountableTopology (A i)] (u : ((i : ι) → A i)ˣ) : ringHaarChar u = ∏ i : ι, ringHaarChar (MulEquiv.piUnits u i)

theorem MeasureTheory.ringHaarChar_restrictedProduct {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] {C : (i : ι) → Subring (A i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [∀ (i : ι), SecondCountableTopology (A i)] [Countable ι] (u : (RestrictedProduct (fun (i : ι) => A i) (fun (i : ι) => ↑(C i)) Filter.cofinite)ˣ) : ringHaarChar u = ∏ᶠ (i : ι), ringHaarChar ((MulEquiv.restrictedProductUnits u) i)

theorem MeasureTheory.ringHaarChar_ModuleFinite {K : Type u_2} {R : Type u_3} [Field K] [Ring R] [Algebra K R] [Module.Finite K R] [TopologicalSpace K] [TopologicalSpace R] [IsTopologicalRing R] [IsModuleTopology K R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] [IsTopologicalRing K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] (t : Kˣ) : ringHaarChar ((Units.map ↑(algebraMap K R)) t) = ringHaarChar ((Units.map ↑(algebraMap K (Fin (Module.finrank K R) → K))) t)

theorem MeasureTheory.ringHaarChar_ModuleFinite_unit {K : Type u_2} {R : Type u_3} [Field K] [Ring R] [Algebra K R] [Module.Finite K R] [TopologicalSpace K] [TopologicalSpace R] [IsTopologicalRing R] [IsModuleTopology K R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] [IsTopologicalRing K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] (t : Kˣ) : ringHaarChar ((Units.map ↑(algebraMap K R)) t) = ringHaarChar t ^ Module.finrank K R