abv_pow

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#IsAbsoluteValue.abv_pow

English

For any a ∈ R and n ∈ ℕ, abv(a^n) = (abv(a))^n.

Русский

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

LaTeX

$$$abv(a^n) = (abv(a))^n$$$

Lean4

theorem abv_pow [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
  (toAbsoluteValue abv).map_pow a n

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

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

Разделы

Аффилиация

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