English
There exists a natural equivalence between Fin(rank K) and the set { w ∈ InfinitePlace(K) : w ≠ w0 }, indexing the units by places of logarithmic embedding.
Русский
Существует натуральное взаимно однозначное соответствие между Fin(rank K) и множеством { w ∈ InfinitePlace(K) : w ≠ w0 }, которое индексирует единицы через логарифмическое вложение.
LaTeX
$$$\\equiv\\; Fin(\\mathrm{rank}\\,K) \\simeq \\{ w : \\mathrm{InfinitePlace}(K) \\mid w \\neq w_0 \\}.$$$
Lean4
/-- An `equiv` between `Fin (rank K)`, used to index the family of units, and `{w // w ≠ w₀}`
the index of the `logSpace`.
-/
def equivFinRank : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ w₀ } :=
Fintype.equivOfCardEq <| by rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]
