norm_negAt

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.norm_negAt

← MathLib Explorer

English

NegAt preserves the global norm of the mixed embedding.

Русский

NegAt сохраняет глобальную норму смешанного вложения.

LaTeX

$$norm_negAt : (negAt s).norm = x.norm$$

Lean4

/-- `negAt` preserves the `norm`. -/
@[simp]
theorem norm_negAt [NumberField K] (x : mixedSpace K) : mixedEmbedding.norm (negAt s x) = mixedEmbedding.norm x :=
  norm_eq_of_normAtPlace_eq (fun w ↦ normAtPlace_negAt _ _ w)

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

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

Разделы

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

Аффилиация

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