English
The mk₂ construction yields a bilinear map with explicit bilinearity properties by construction.
Русский
Конструкция mk₂ задаёт билинейное отображение с явными свойствами билинейности по построению.
LaTeX
$$$ mk₂ : M \\toₗ[R] Nₗ \\toₗ[R] Pₗ $ is bilinear$$
Lean4
/-- Create a bilinear map from a function that is linear in each component.
This is a shorthand for `mk₂'` for the common case when `R = S`. -/
def mk₂ (f : M → Nₗ → Pₗ) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
(H2 : ∀ (c : R) (m n), f (c • m) n = c • f m n) (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
(H4 : ∀ (c : R) (m n), f m (c • n) = c • f m n) : M →ₗ[R] Nₗ →ₗ[R] Pₗ :=
mk₂' R R f H1 H2 H3 H4
