map_pow

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.map_pow

English

For any x and natural n, v(x^n) = v(x)^n.

Русский

Для любого x и натурального n выполняется v(x^n) = v(x)^n.

LaTeX

$$$ v(x^n) = v(x)^n $$$

Lean4

protected theorem map_pow : ∀ (x) (n : ℕ), v (x ^ n) = v x ^ n :=
  v.toMonoidWithZeroHom.toMonoidHom.map_pow

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

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

Разделы

Аффилиация

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