English
The total number of infinite places is the sum of real and complex places: card(InfinitePlace(K)) = nrRealPlaces(K) + nrComplexPlaces(K).
Русский
Общее число бесконечных мест равно сумме реальных и комплексных мест.
LaTeX
$$Fintype.card(\mathrm{InfinitePlace}(K)) = \mathrm{nrRealPlaces}(K) + \mathrm{nrComplexPlaces}(K)$$
Lean4
/-- The infinite part of the product formula : for `x ∈ K`, we have `Π_w ‖x‖_w = |norm(x)|` where
`‖·‖_w` is the normalized absolute value for `w`. -/
theorem prod_eq_abs_norm (x : K) : ∏ w : InfinitePlace K, w x ^ mult w = abs (Algebra.norm ℚ x) := by
classical
convert (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm
· rw [norm_prod, ←
Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖) (fun φ => ‖φ x‖) fun _ => by
simp [RingHom.equivRatAlgHom_apply]]
rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) : ‖φ x‖ = w x := by
rw [← (Finset.mem_filter.mp hφ).2, apply]
simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]
· rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
