coe_powMonoidWithZeroHom — Mathlib

English

Let hn be a nonzero natural number. The map x ↦ x^n is the function underlying the monoid-with-zero endomorphism powMonoidWithZeroHom hn, i.e., it acts by x ↦ x^n on M₀.

Русский

Пусть hn — ненулевое натуральное число. Отображение x ↦ x^n является функцией, лежащей в основе эндоморфизма моноида с нулём powMonoidWithZeroHom hn, то есть действует как x ↦ x^n на M₀.

LaTeX

$$$ (powMonoidWithZeroHom hn) : M_0 \to_*_0 M_0 \;\text{и}\; (powMonoidWithZeroHom hn)(x) = x^n \text{ для всех } x. $$$

Lean4

@[simp]
theorem coe_powMonoidWithZeroHom : (powMonoidWithZeroHom hn : M₀ → M₀) = fun x ↦ x ^ n :=
  rfl

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