card — Mathlib

English

The number of embeddings of a number field equals its finitary dimension finrank over ℚ.

Русский

Число вложений числа поля равно его конечной размерности над ℚ.

LaTeX

$$$\mathrm{Fintype}.card(K \to+* A) = \mathrm{finrank}\; \mathbb{Q} \; K$$$

Lean4

/-- The number of embeddings of a number field is equal to its finrank. -/
theorem card : Fintype.card (K →+* A) = finrank ℚ K := by
  rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]

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