mapL_pow — Mathlib

English

Reiterating the identity preservation: mapL (i ↦ id_Ei) equals the identity on the tensor product.

Русский

Повторно утверждается сохранение тождества: mapL (i ↦ id_Ei) = id_{⨂ i, E_i}.

LaTeX

$$$ \\mathrm{mapL}(\\lambda i, \\mathrm{id}_{E_i}) = \\mathrm{id}_{\\bigotimes i, E_i} $$$

Lean4

@[simp]
protected theorem mapL_pow (f : Π i, E i →L[𝕜] E i) (n : ℕ) : mapL (f ^ n) = mapL f ^ n :=
  MonoidHom.map_pow mapLMonoidHom f n

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