inter_ball_finite — Mathlib

English

If K/F is a CM-extension, then K is a CM-field.

Русский

Если K/F — CM-расширение, то K является CM-полем.

LaTeX

$$$K/F\\text{ is CM-extension} \\Rightarrow K\\text{ is CM-field}$$$

Lean4

theorem inter_ball_finite [NumberField K] (r : ℝ) :
    ((integerLattice K : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite :=
  by
  obtain hr | _ := lt_or_ge r 0
  · simp [Metric.closedBall_eq_empty.2 hr]
  · have heq : ∀ x, canonicalEmbedding K x ∈ Metric.closedBall 0 r ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r := by intro x;
      rw [← norm_le_iff, mem_closedBall_zero_iff]
    convert (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)
    ext; constructor
    · rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩
      exact ⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩
    · rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩
      exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩

Похожие утверждения