powMonoidWithZeroHom_apply — Mathlib

English

For hn ≠ 0 and a ∈ M₀, the endomorphism powMonoidWithZeroHom hn evaluated at a equals a^n; i.e., (powMonoidWithZeroHom hn) a = a^n.

Русский

При hn ≠ 0 и любом a ∈ M₀ отображение powMonoidWithZeroHom hn, применённое к a, даёт a^n; то есть (powMonoidWithZeroHom hn) a = a^n.

LaTeX

$$$ (powMonoidWithZeroHom hn) a = a^n. $$$

Lean4

@[simp]
theorem powMonoidWithZeroHom_apply (a : M₀) : powMonoidWithZeroHom hn a = a ^ n :=
  rfl

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