extensionEmbedding_coe

Mathlib.NumberTheory.NumberField.InfinitePlace.Completion

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.Completion.extensionEmbedding_coe

English

The real-infinite place property holds for Rat: the infinite place is real.

Русский

Свойство IsReal выполняется для Rat: бесконечное место вещественное.

LaTeX

$$isReal_infinitePlace$$

Lean4

@[simp]
theorem extensionEmbedding_coe (x : K) : extensionEmbedding v x = v.embedding x :=
  extensionEmbedding_of_comp_coe v.norm_embedding_eq x

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

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

Разделы

Аффилиация

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