map_eq — Mathlib

English

The heterobasic version of map distributes over its arguments: map (f2 ∘ f1) (g2 ∘ g1) equals map f2 g2 composed with map f1 g1.

Русский

Гетеробазовая версия map распределяется по своим аргументам: map (f2 ∘ f1) (g2 ∘ g1) = map f2 g2 ∘ map f1 g1.

LaTeX

$$$\text{map}(f_2 \circ f_1, g_2 \circ g_1) = (\text{map}(f_2,g_2)) \circ (\text{map}(f_1,g_1))$$$

Lean4

/-- The heterobasic version of `map` coincides with the regular version. -/
theorem map_eq (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f g = TensorProduct.map f g :=
  rfl

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