val_pow_eq_pow_val

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#Units.val_pow_eq_pow_val

English

For a unit a ∈ α^× and n ∈ ℕ, the underlying element of a^n equals a^n in α.

Русский

Для единицы a ∈ α^× и n ∈ ℕ подмножество элемента a^n совпадает с a^n в α.

LaTeX

$$$\uparrow(a^n) = (a^n : \alpha)$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem val_pow_eq_pow_val (n : ℕ) : ↑(a ^ n) = (a ^ n : α) :=
  rfl

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

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

Разделы

Аффилиация

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