expMap_symm_apply

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

English

The symmetry expMap.symm is continuous in the real-space variables, consistent with exp and log maps.

Русский

Симметричное отображение expMap.symm непрерывно по вещественным переменным.

LaTeX

$$$\\text{Continuous}(\\expMap.symm)$$$

Lean4

@[simp]
theorem expMap_symm_apply (x : realSpace K) (w : InfinitePlace K) : expMap.symm x w = ↑w.mult * Real.log (x w) :=
  rfl

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

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

Разделы

Аффилиация

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