map_zpow₀ — Mathlib

English

Given a map f between group-with-zero structures, f(x^n) = f(x)^n for all integers n.

Русский

Для отображения f между группами с нулём верно f(x^n) = f(x)^n для всех целых n.

LaTeX

$$$f(x^{n}) = f(x)^{n}$ for all $n \\in \\mathbb{Z}$$$

Lean4

/-- If a monoid homomorphism `f` between two `GroupWithZero`s maps `0` to `0`, then it maps `x^n`,
`n : ℤ`, to `(f x)^n`. -/
@[simp]
theorem map_zpow₀ {F G₀ G₀' : Type*} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀']
    [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) : f (x ^ n) = f x ^ n :=
  map_zpow' f (map_inv₀ f) x n

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