mulSupport_finite — Mathlib

English

For x ∈ K nonzero, the set of finite places where w x ≠ 0 is finite.

Русский

Для не нулевого x ∈ K множество мест, где w x ≠ 0, конечно.

LaTeX

$$$\\{w : FinitePlace(K) \\mid w x \\ne 0\\}$ is finite$$

Lean4

theorem mulSupport_finite {x : K} (h_x_nezero : x ≠ 0) : (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite :=
  by
  rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩
  simp_all only [ne_eq, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, map_div₀]
  obtain ⟨ha, hb⟩ := h_x_nezero
  simp_rw [← RingOfIntegers.coe_eq_algebraMap]
  apply ((mulSupport_finite_int ha).union (mulSupport_finite_int hb)).subset
  intro w
  simp only [Function.mem_mulSupport, ne_eq, Set.mem_union]
  contrapose!
  simp +contextual only [ne_eq, one_ne_zero, not_false_eq_true, div_self, implies_true]

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