logMap_zero

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

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

English

The log map sends 0 to 0 and 1 to 0 in the mixed embedding context.

Русский

Лог-карта отправляет 0 в 0 и 1 в 0 в контексте смешанного вложения.

LaTeX

$$$\logMap(0) = 0$ and $\logMap(1) = 0$$$

Lean4

@[simp]
theorem logMap_zero : logMap (0 : mixedSpace K) = 0 := by ext; simp

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

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

Разделы

Аффилиация

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