mk_embedding

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

For any infinite place w, mk(embedding w) recovers w exactly.

Русский

Для любого бесконечного места w, mk(embedding w) восстанавливает w точно.

LaTeX

$$mk (embedding w) = w$$

Lean4

@[simp]
theorem mk_embedding (w : InfinitePlace K) : mk (embedding w) = w :=
  Subtype.ext w.2.choose_spec

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

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

Разделы

Аффилиация

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