map_pow — Mathlib

English

There is a Monoid Hom from endomorphism families to endomorphisms of the tensor product, given by map.

Русский

Существует гомоморфизм моноидов от семей эндоморфизмов к эндоморфизмам тензорного произведения, задаваемый map.

LaTeX

$$$\mathrm{mapMonoidHom} : (\Pi i,\, s_i \to s_i) \to^* (\otimes_i s_i \to s_i)$ with the properties described by map and map_one.$$

Lean4

@[simp]
protected theorem map_pow (f : Π i, s i →ₗ[R] s i) (n : ℕ) : map (f ^ n) = map f ^ n :=
  MonoidHom.map_pow mapMonoidHom _ _

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