ppow_eq_pow

Mathlib.Algebra.Group.PNatPowAssoc

URI: https://scilib.ai/kg/mathlib#ppow_eq_pow

← MathLib Explorer

English

For x ∈ M, n ∈ ℕ+, x^n = x^(n : ℕ).

Русский

Для x ∈ M и n ∈ ℕ+ выполняется x^n = x^(n : ℕ).

LaTeX

$$$x^{n} = x^{\\; (n : \\mathbb{N})}$$$

Lean4

theorem ppow_eq_pow [Monoid M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+) : x ^ n = x ^ (n : ℕ) := by
  induction n with
  | one => rw [ppow_one, PNat.one_coe, pow_one]
  | succ k hk => rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

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

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

Разделы

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

Аффилиация

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