English
The number of embeddings φ with mk φ equal to a fixed w equals mult(w): #{φ | mk φ = w} = mult w.
Русский
Число вложений φ, удовлетворяющих mk φ = w, равно mult(w).
LaTeX
$$$\#\{\varphi : K \to \mathbb{C} \mid \mathrm{mk}(\varphi) = w\} = \operatorname{mult}(w)$$$
Lean4
theorem card_filter_mk_eq [NumberField K] (w : InfinitePlace K) : #{φ | mk φ = w} = mult w :=
by
conv_lhs =>
congr; congr; ext
rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)), Finset.mem_univ, ite_true, mult]
split_ifs with hw
· rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent, Finset.card_singleton]
· refine Finset.card_pair ?_
rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
