equivReindex — Mathlib

English

There is a canonical equivalence between embeddings of K into ℂ and the index set of a chosen basis of the ring of integers of K.

Русский

Существует каноническое эквивалентность между вложениями K в ℂ и индексным множеством выбранной базы кольца целых чисел K.

LaTeX

$$$$\\text{equivReindex} : (K \\to_+^* \\mathbb{C}) \\simeq \\text{ChooseBasisIndex } \\mathbb{Z} (\\mathcal{O}_K).$$$$

Lean4

/-- An equivalence between the set of embeddings of `K` into `ℂ` and the
  index set of the chosen basis of the ring of integers of `K`. -/
abbrev equivReindex : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) :=
  Fintype.equivOfCardEq <| by rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]

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