structure IsRadonMeasure {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] [T2Space X] [LocallyCompactSpace X] (μ : MeasureTheory.Measure X) : Prop

• isFiniteMeasureOnCompacts : MeasureTheory.IsFiniteMeasureOnCompacts μ
• regular : μ.Regular
• innerRegular : μ.InnerRegular

theorem compact_group_finite_measure (G : Type u_1) [AddCommGroup G] [TopologicalSpace G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] : MeasureTheory.IsFiniteMeasure μ

theorem weil_uniqueness (G : Type u_1) [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ ν : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] : ∃ (c : ENNReal), c ≠ 0 ∧ c ≠ ⊤ ∧ ν = c • μ

def mulLeftContinuousAddEquiv {K : Type u_1} [NormedField K] {a : K} (ha : a ≠ 0) : K ≃ₜ+ K

@[simp]

theorem mulLeftContinuousAddEquiv_apply {K : Type u_1} [NormedField K] {a : K} (ha : a ≠ 0) (x : K) : (mulLeftContinuousAddEquiv ha) x = a * x

theorem mulLeftContinuousAddEquiv_preimage_smul {K : Type u_1} [NormedField K] {a : K} (ha : a ≠ 0) (S : Set K) : ⇑(mulLeftContinuousAddEquiv ha) ⁻¹' (a • S) = S

theorem mulLeftContinuousAddEquiv_symm {K : Type u_1} [NormedField K] {a : K} (ha : a ≠ 0) : (mulLeftContinuousAddEquiv ha).symm = mulLeftContinuousAddEquiv ⋯

theorem proposition_13_16_haar_scaling (K : Type u_1) [NormedField K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsAddHaarMeasure] [μ.Regular] (a : K) (ha : a ≠ 0) (S : Set K) : μ (a • S) = ↑(MeasureTheory.addEquivAddHaarChar (mulLeftContinuousAddEquiv ha)) * μ S

theorem distribHaarChar_eq_addEquivAddHaarChar_mulLeft {K : Type u_1} [NormedField K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] {a : K} (ha : a ≠ 0) : (MeasureTheory.distribHaarChar K) (Units.mk0 a ha) = MeasureTheory.addEquivAddHaarChar (mulLeftContinuousAddEquiv ha)

theorem units_smul_closedBall_zero_one {K : Type u_1} [NormedField K] (g : Kˣ) : ↑g • Metric.closedBall 0 1 = Metric.closedBall 0 ‖↑g‖

theorem units_smul_ball_zero_one {K : Type u_1} [NormedField K] (g : Kˣ) : ↑g • Metric.ball 0 1 = Metric.ball 0 ‖↑g‖

theorem dvr_index_eq_nnnorm_inv (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] (g : Kˣ) (hg : ‖↑g‖ < 1) (reps : Finset K) (hcover : Metric.closedBall 0 1 = ⋃ a ∈ reps, Metric.closedBall a ‖↑g‖) (hdisjoint : ∀ a ∈ reps, ∀ b ∈ reps, a ≠ b → Disjoint (Metric.closedBall a ‖↑g‖) (Metric.closedBall b ‖↑g‖)) : ↑reps.card * ‖↑g‖₊ = 1

theorem haar_closedBall_eq_nnnorm_mul_of_norm_lt_one (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsAddHaarMeasure] (g : Kˣ) (hg : ‖↑g‖ < 1) : μ (Metric.closedBall 0 ‖↑g‖) = ↑‖↑g‖₊ * μ (Metric.closedBall 0 1)

theorem distribHaarChar_eq_nnnorm_of_norm_lt_one (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] (g : Kˣ) (hg : ‖↑g‖ < 1) : (MeasureTheory.distribHaarChar K) g = ‖↑g‖₊

theorem distribHaarChar_eq_nnnorm_dvr_helper (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] (g : Kˣ) (hg : ‖↑g‖ < 1) : (MeasureTheory.distribHaarChar K) g = ‖↑g‖₊

theorem distribHaarChar_eq_nnnorm_ultrametric_axiom (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] (g : Kˣ) (hg : ‖↑g‖ ≤ 1) : (MeasureTheory.distribHaarChar K) g = ‖↑g‖₊

theorem distribHaarChar_eq_nnnorm_ultrametric (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] (g : Kˣ) : (MeasureTheory.distribHaarChar K) g = ‖↑g‖₊

theorem distribHaarChar_eq_nnnorm_of_ultrametric (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [IsUltrametricDist K] (g : Kˣ) (_hg : ‖↑g‖ ≤ 1) : (MeasureTheory.distribHaarChar K) g = ‖↑g‖₊

theorem distribHaarChar_eq_nnnorm_of_norm_le_one_aux (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] [IsUltrametricDist K] (g : Kˣ) (hg : ‖↑g‖ ≤ 1) : (MeasureTheory.distribHaarChar K) g = ‖↑g‖₊

theorem dvr_haar_char_eq_nnnorm_of_norm_le_one (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] [IsUltrametricDist K] (a : K) (ha : a ≠ 0) (ha_le : ‖a‖ ≤ 1) : MeasureTheory.addEquivAddHaarChar (mulLeftContinuousAddEquiv ha) = ‖a‖₊

theorem addEquivAddHaarChar_mulLeft_eq_nnnorm (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] [IsUltrametricDist K] (a : K) (ha : a ≠ 0) : MeasureTheory.addEquivAddHaarChar (mulLeftContinuousAddEquiv ha) = ‖a‖₊

theorem proposition_13_16_nonarchimedean (K : Type u_1) [NontriviallyNormedField K] [LocallyCompactSpace K] [MeasurableSpace K] [BorelSpace K] [IsUltrametricDist K] (μ : MeasureTheory.Measure K) [μ.IsAddHaarMeasure] [μ.Regular] (a : K) (ha : a ≠ 0) (S : Set K) : μ (a • S) = ↑‖a‖₊ * μ S

def IsNormalizedAbsVal {K : Type u_1} [Field K] [TopologicalSpace K] [MeasurableSpace K] [BorelSpace K] [LocallyCompactSpace K] [T2Space K] (f : K → ℝ) : Prop

theorem isNormalizedAbsVal_unique {K : Type u_1} [Field K] [TopologicalSpace K] [MeasurableSpace K] [BorelSpace K] [LocallyCompactSpace K] [T2Space K] [IsTopologicalAddGroup K] (f g : K → ℝ) (hf : IsNormalizedAbsVal f) (hg : IsNormalizedAbsVal g) : f = g

theorem haar_scaling_det (K_v : Type u_1) [Field K_v] [TopologicalSpace K_v] [MeasurableSpace K_v] [BorelSpace K_v] [LocallyCompactSpace K_v] [T2Space K_v] (L_w : Type u_2) [Field L_w] [TopologicalSpace L_w] [MeasurableSpace L_w] [BorelSpace L_w] [LocallyCompactSpace L_w] [T2Space L_w] [IsTopologicalAddGroup L_w] [Algebra K_v L_w] [FiniteDimensional K_v L_w] (normAbsVal_v : K_v → ℝ) (hv : IsNormalizedAbsVal normAbsVal_v) (μ : MeasureTheory.Measure L_w) [μ.IsAddHaarMeasure] (f : L_w →ₗ[K_v] L_w) (S : Set L_w) : μ (⇑f '' S) = ENNReal.ofReal (normAbsVal_v (LinearMap.det f)) * μ S

theorem haar_scaling_algebra_norm (K_v : Type u_1) [Field K_v] [TopologicalSpace K_v] [MeasurableSpace K_v] [BorelSpace K_v] [LocallyCompactSpace K_v] [T2Space K_v] (L_w : Type u_2) [Field L_w] [TopologicalSpace L_w] [MeasurableSpace L_w] [BorelSpace L_w] [LocallyCompactSpace L_w] [T2Space L_w] [IsTopologicalAddGroup L_w] [Algebra K_v L_w] [FiniteDimensional K_v L_w] (normAbsVal_v : K_v → ℝ) (hv : IsNormalizedAbsVal normAbsVal_v) (μ : MeasureTheory.Measure L_w) [μ.IsAddHaarMeasure] (a : L_w) (S : Set L_w) : μ ((fun (x : L_w) => a * x) '' S) = ENNReal.ofReal (normAbsVal_v ((Algebra.norm K_v) a)) * μ S

theorem norm_composition_isNormalizedAbsVal (K_v : Type u_1) [Field K_v] [TopologicalSpace K_v] [MeasurableSpace K_v] [BorelSpace K_v] [LocallyCompactSpace K_v] [T2Space K_v] (L_w : Type u_2) [Field L_w] [TopologicalSpace L_w] [MeasurableSpace L_w] [BorelSpace L_w] [LocallyCompactSpace L_w] [T2Space L_w] [IsTopologicalAddGroup L_w] [Algebra K_v L_w] [FiniteDimensional K_v L_w] (normAbsVal_v : K_v → ℝ) (hv : IsNormalizedAbsVal normAbsVal_v) : IsNormalizedAbsVal fun (x : L_w) => normAbsVal_v ((Algebra.norm K_v) x)

theorem lemma_13_19 (K_v : Type u_1) [Field K_v] [TopologicalSpace K_v] [MeasurableSpace K_v] [BorelSpace K_v] [LocallyCompactSpace K_v] [T2Space K_v] (L_w : Type u_2) [Field L_w] [TopologicalSpace L_w] [MeasurableSpace L_w] [BorelSpace L_w] [LocallyCompactSpace L_w] [T2Space L_w] [IsTopologicalAddGroup L_w] [Algebra K_v L_w] [FiniteDimensional K_v L_w] (normAbsVal_v : K_v → ℝ) (hv : IsNormalizedAbsVal normAbsVal_v) (normAbsVal_w : L_w → ℝ) (hw : IsNormalizedAbsVal normAbsVal_w) (x : L_w) : normAbsVal_w x = normAbsVal_v ((Algebra.norm K_v) x)

class IsGlobalField (K : Type u_1) [Field K] : Type (max (max u_1 (u_2 + 1)) (u_3 + 1))

• PlaceType : Type u_2
• place_nonempty : Nonempty (PlaceType K)
• Completion : PlaceType K → Type u_3
• completionField (v : PlaceType K) : Field (Completion v)
• completionTopologicalSpace (v : PlaceType K) : TopologicalSpace (Completion v)
• completionLocallyCompact (v : PlaceType K) : LocallyCompactSpace (Completion v)
• completionNontrivial (v : PlaceType K) : Nontrivial (Completion v)
• absVal : PlaceType K → AbsoluteValue K ℝ
• exponent : PlaceType K → ℝ
• exponent_pos (v : PlaceType K) : 0 < exponent v
• normAbsVal : PlaceType K → K → ℝ
• normAbsVal_nonneg (v : PlaceType K) (x : K) : 0 ≤ normAbsVal v x
• normAbsVal_eq (v : PlaceType K) (x : K) : normAbsVal v x = (absVal v) x ^ exponent v
• normAbsVal_eq_one_of_finite (x : K) : x ≠ 0 → {v : PlaceType K | normAbsVal v x ≠ 1}.Finite
• product_formula (x : K) : x ≠ 0 → ∏ᶠ (v : PlaceType K), normAbsVal v x = 1

theorem theorem_13_21_product_formula_global (K : Type u_1) [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : (∏ w : NumberField.InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : NumberField.FinitePlace K), w x = 1

theorem artin_whaples_classification (K : Type u_1) [Field K] [IsGlobalField K] : (∃ (x : Algebra ℚ K), FiniteDimensional ℚ K) ∨ ∃ (Fq : Type u_2) (x : Field Fq) (x_1 : Fintype Fq) (x_2 : Algebra (RatFunc Fq) K), FiniteDimensional (RatFunc Fq) K