eq_iff_eq — Mathlib

English

Let x ∈ K and r ∈ ℝ. The condition that w(x) = r for every infinite place w is equivalent to the condition that |φ(x)| = r for every ring hom φ: K →+* ℂ.

Русский

Пусть x ∈ K и r ∈ ℝ. Условие, что w(x) = r для каждого бесконечного места w, эквивалентно тому, что |φ(x)| = r для каждого кольцевого гомоморфа φ: K →+* ℂ.

LaTeX

$$$\\forall x \\in K, \\forall r \\in \\mathbb{R},\\; (\\\\forall w \\\\in \\\\mathrm{InfinitePlace}(K), w x = r) \\\\iff (\\\\forall \\varphi \\\\colon K \\\\to+* \\\\mathbb{C}, \\\\|\\\\varphi x\\\\| = r).$$$$

Lean4

theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : InfinitePlace K, w x = r) ↔ ∀ φ : K →+* ℂ, ‖φ x‖ = r :=
  ⟨fun hw φ => hw (mk φ), by rintro hφ ⟨w, ⟨φ, rfl⟩⟩; exact hφ φ⟩

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