instNonemptyRingHom

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

English

There exists at least one ring homomorphism from K to A when A is alg closed and suitable conditions hold.

Русский

Существует хотя бы одно вложение кольца K в A при подходящих условиях.

LaTeX

$$Nonempty (RingHom K A)$$

Lean4

instance : Nonempty (K →+* A) :=
  by
  rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]
  exact Module.finrank_pos

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

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

Разделы

Аффилиация

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