coe_zpow

Mathlib.NumberTheory.NumberField.Units.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.Units.coe_zpow

← MathLib Explorer

English

The image of −1 in the unit group is −1 in the base field under the embedding.

Русский

Изображение −1 в единицах переходит в −1 в базовом поле через вложение.

LaTeX

$$$(-1)_{(𝓞K)^{×}} \mapsto -1_K$$$

Lean4

theorem coe_zpow (x : (𝓞 K)ˣ) (n : ℤ) : (↑(x ^ n) : K) = (x : K) ^ n :=
  by
  change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _
  exact map_zpow _ x n

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

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

Разделы

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

Аффилиация

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