toEnd_pow — Mathlib

English

Raising a centroid hom to a natural power corresponds to raising its endomorphism to the same power: (x^n).toEnd = x.toEnd^n.

Русский

Возведение центроид-гомоморфизма в натуральную степень соответствует возведению его концевого отображения в ту же степень: (x^n).toEnd = x.toEnd^n.

LaTeX

$$theorem toEnd_pow (x : CentroidHom α) (n : ℕ) : (x ^ n).toEnd = x.toEnd ^ n$$

Lean4

@[simp]
theorem toEnd_pow (x : CentroidHom α) (n : ℕ) : (x ^ n).toEnd = x.toEnd ^ n :=
  rfl

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