IsPowMul — Mathlib

English

A function f: R → ℝ is power-multiplicative if f(a^n) = f(a)^n for all a and all n ≥ 1.

Русский

Функция f: R → ℝ удовлетворяет свойству степенного умножения, если f(a^n) = f(a)^n для всех a и n ≥ 1.

LaTeX

$$$\forall a\in R,\forall n\in\mathbb{N},\ 1 \le n \Rightarrow f(a^n) = f(a)^n$$$

Lean4

/-- A function `f : R → ℝ` is power-multiplicative if for all `r ∈ R` and all positive `n ∈ ℕ`,
`f (r ^ n) = (f r) ^ n`. -/
def IsPowMul {R : Type*} [Pow R ℕ] (f : R → ℝ) :=
  ∀ (a : R) {n : ℕ}, 1 ≤ n → f (a ^ n) = f a ^ n

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