const_pow

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.const_pow

English

For any x ∈ β and n ∈ ℕ, the nth power of the constant CauSeq at x equals the constant CauSeq at x^n: const(x^n) = (const x)^n.

Русский

Для любого x ∈ β и n ∈ ℕ степенная константной последовательности даёт: const(x^n) = (const x)^n.

LaTeX

$$$\mathrm{const}(x^n) = (\mathrm{const}(x))^n$$$

Lean4

theorem const_pow (x : β) (n : ℕ) : const (x ^ n) = const x ^ n :=
  rfl

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

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

Разделы

Аффилиация

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