instFintypeRingHom

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

URI: https://scilib.ai/kg/mathlib#NumberField.Embeddings.instFintypeRingHom

← MathLib Explorer

English

There are finitely many embeddings of a number field into a fixed target field A.

Русский

Число вложений числа поля K в A конечно.

LaTeX

$$$\#\mathrm{RingHom}(K,A) < \infty$$$

Lean4

/-- There are finitely many embeddings of a number field. -/
noncomputable instance : Fintype (K →+* A) :=
  Fintype.ofEquiv (K →ₐ[ℚ] A) RingHom.equivRatAlgHom.symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru