coe_pow

Mathlib.NumberTheory.NumberField.Units.Basic

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

English

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

Русский

Образ единицы 1 в базовом поле under вложение равен 1 в K.

LaTeX

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

Lean4

theorem coe_pow (x : (𝓞 K)ˣ) (n : ℕ) : ((x ^ n : (𝓞 K)ˣ) : K) = (x : K) ^ n := by rw [← map_pow, ← val_pow_eq_pow_val]

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

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

Разделы

Аффилиация

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