map_pow — Mathlib

English

Let abv be an absolute value from R to S. Then for every a ∈ R and every n ∈ ℕ, |a^n| = |a|^n.

Русский

Пусть abv является абсолютной величиной от R в S. Тогда для любого a ∈ R и любого n ∈ ℕ выполняется |a^n| = |a|^n.

LaTeX

$$$\\forall a \\in R, \\forall n \\in \\mathbb{N},\\; \\operatorname{abv}(a^n) = \\operatorname{abv}(a)^n$$$

Lean4

@[simp]
protected theorem map_pow (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
  abv.toMonoidHom.map_pow a n

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