rpowMonoidHom — Mathlib

English

For each real r, the map x ↦ x^r defines a monoid endomorphism of the multiplicative monoid of nonnegative reals.

Русский

Для фиксированного вещественного r отображение x ↦ x^r является однородным гомоморфизмом по умонодной структуре умножения на неотрицательных вещественных числах.

LaTeX

$$∀ r ∈ ℝ, (x ↦ x^{r}) : ℝ_{≥0} → ℝ_{≥0} satisfies (x y)^{r} = x^{r} y^{r} и 1^{r} = 1$$

Lean4

/-- `rpow` as a `MonoidHom` -/
@[simps]
def rpowMonoidHom (r : ℝ) : ℝ≥0 →* ℝ≥0 where
  toFun := (· ^ r)
  map_one' := one_rpow _
  map_mul' _x _y := mul_rpow

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