isometry_extensionEmbedding

Mathlib.NumberTheory.NumberField.InfinitePlace.Completion

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

← MathLib Explorer

English

The embedding extensionEmbedding is an isometry.

Русский

Встраивание является изометрией.

LaTeX

$$Isometry (extensionEmbedding v)$$

Lean4

/-- The embedding `v.Completion →+* ℂ` is an isometry. -/
theorem isometry_extensionEmbedding : Isometry (extensionEmbedding v) :=
  Isometry.of_dist_eq (extensionEmbedding_dist_eq_of_comp v.norm_embedding_eq)

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

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

Разделы

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

Аффилиация

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