isPowMul — Mathlib

English

A multiplicative ring norm is power-multiplicative: f(x^n) = f(x)^n for n ∈ ℕ.

Русский

Умножаемая кольцевая норма является степенно-мультипликативной: f(x^n) = f(x)^n для натуральных n.

LaTeX

$$$IsPowMul\\;f$$$

Lean4

/-- A multiplicative ring norm is power-multiplicative. -/
theorem isPowMul {A : Type*} [Ring A] (f : MulRingNorm A) : IsPowMul f := fun x n hn =>
  by
  cases n
  · cutsat
  · rw [map_pow]

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