English
There is a natural way to compose a bilinear map with a linear map to obtain a new bilinear map: (f ∘₂ g)(m)(n) = g(f(m)(n)). The operation preserves addition and scalar action.
Русский
Существует естественный способ композиции билинейной карты с линейной, чтобы получить новую билинейную карту: (f ∘₂ g)(m)(n) = g(f(m)(n)). Операция сохраняет сложение и скалярное умножение.
LaTeX
$$$$(f \; .compr_2\; g)\, (m)\, (n) = g\bigl(f(m)(n)\bigr).$$$$
Lean4
@[simp]
theorem compr₂_apply [Module R A] [Module A M] [Module A Qₗ] [SMulCommClass R A Qₗ] [IsScalarTower R A Qₗ]
[IsScalarTower R A Pₗ] (f : M →ₗ[A] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[A] Qₗ) (m : M) (n : Nₗ) : f.compr₂ g m n = g (f m n) :=
rfl
