English
An embedding into a normed division ring defines a place of K.
Русский
Вложение K в нормированное деление кольца задаёт место поля K.
LaTeX
$$place : AbsoluteValue K Real$$
Lean4
/-- An algebraic integer whose conjugates are all of norm one is a root of unity. -/
theorem pow_eq_one_of_norm_eq_one {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ φ : K →+* A, ‖φ x‖ = 1) :
∃ (n : ℕ) (_ : 0 < n), x ^ n = 1 :=
by
obtain ⟨a, -, b, -, habne, h⟩ :=
@Set.Infinite.exists_ne_map_eq_of_mapsTo _ _ _ _ (x ^ · : ℕ → K) Set.infinite_univ
(by exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩) (finite_of_norm_le K A (1 : ℝ))
wlog hlt : b < a
· exact this K A hxi hx b a habne.symm h.symm (habne.lt_or_gt.resolve_right hlt)
refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h
refine h.resolve_right fun hp => ?_
specialize hx (IsAlgClosed.lift (R := ℚ)).toRingHom
rw [pow_eq_zero hp, map_zero, norm_zero] at hx; norm_num at hx
