powMonoidWithZeroHom — Mathlib

English

Let M₀ be a commutative MonoidWithZero and let n ∈ ℕ with n ≠ 0. The map x ↦ x^n defines a MonoidWithZeroEndomorphism of M₀; in other words, x ↦ x^n preserves multiplication and sends 0 to 0.

Русский

Пусть M₀ — коммутативный моноид с нулём и дано натуральное число n ≠ 0. Отображение x ↦ x^n задаёт эндоморфизм моноидов с нулём на M₀; то есть сохраняет умножение и нуль.

LaTeX

$$$ (\forall x \in M_0)\, (x^n) = x^n. $$$

Lean4

/-- We define `x ↦ x^n` (for positive `n : ℕ`) as a `MonoidWithZeroHom` -/
def powMonoidWithZeroHom : M₀ →*₀ M₀ :=
  { powMonoidHom n with map_zero' := zero_pow hn }

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