mapMonoidHom — Mathlib

English

The map commutes with powers: map(f^n) = (map f)^n.

Русский

Отображение коммутирует с возведением в степень: map(f^n) = (map f)^n.

LaTeX

$$$\mathrm{map}(f^{n}) = (\mathrm{map} (f))^{n}$$$

Lean4

/-- Upgrading `PiTensorProduct.map` to a `MonoidHom` when `s = t`. -/
@[simps]
def mapMonoidHom : (Π i, s i →ₗ[R] s i) →* ((⨂[R] i, s i) →ₗ[R] ⨂[R] i, s i)
    where
  toFun := map
  map_one' := PiTensorProduct.map_one
  map_mul' := PiTensorProduct.map_mul

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