mapBilinear_apply — Mathlib

English

For f and g, applying homTensorHomMap to f ⊗ g yields map f g.

Русский

Для отображений f и g применение homTensorHomMap к f ⊗ g даёт отображение map f g.

LaTeX

$$$\mathrm{homTensorHomMap\_apply} \; (f:\ M \to_A P)\ (g:\ N \to_R Q) : \mathrm{homTensorHomMap}\ R A B M N P Q (f \otimes g) = \mathrm{map} f g$$$

Lean4

@[simp]
theorem mapBilinear_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : mapBilinear R A B M N P Q f g = map f g :=
  rfl

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