factorization_pow

Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

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

← MathLib Explorer

English

For any x and n, factorization(x^n) = n · factorization(x).

Русский

Для любого x и n: factorization(x^n) = n · factorization(x).

LaTeX

$$$\\text{factorization}(x^n) = n \\cdot \\text{factorization}(x)$$$

Lean4

/-- For any `p`, the power of `p` in `x^n` is `n` times the power in `x` -/
theorem factorization_pow {x : α} {n : ℕ} : factorization (x ^ n) = n • factorization x :=
  by
  ext
  simp [factorization]

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

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

Разделы

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

Аффилиация

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