equivFinRank — Mathlib

English

There is a fixed equivalence between Fin(rank K) and the set of infinite places w ≠ w0, identifying the (unit) rank of the field with those places.

Русский

Существует фиксированное биективное соответствие между Fin(rank K) и множеством бесконечных мест w, удовлетворяющих w ≠ w0, тем самым устанавливая соответствие ранга единиц полей множеству таких мест.

LaTeX

$$$\operatorname{Fin}(\operatorname{rank} K) \cong \{ w : \mathrm{InfinitePlace}(K) \mid w \neq w_0 \ \}$$$

Lean4

/-- A fixed equiv between `Fin (rank K)` and `{w : InfinitePlace K // w ≠ w₀}`.
-/
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]

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