English
The construction mk₂ builds a bilinear map from a function f: M → N × P with bilinearity hypotheses; evaluating at x, y yields f(x, y).
Русский
Из функции f, удовлетворяющей билинейности, через mk₂ можно построить билинейное отображение, и его применение дает f(x,y).
LaTeX
$$$ (mk₂ R f H1 H2 H3 H4)\\; x\\; y = f(x,y) $$$
Lean4
/-- `LinearMap.flip` as an isomorphism of modules. -/
def lflip {R₀ : Type*} [Semiring R₀] [Module R₀ P] [SMulCommClass S₂ R₀ P] [SMulCommClass R₂ R₀ P] :
(M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) ≃ₗ[R₀] (N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P)
where
toFun := flip
invFun := flip
map_add' _ _ := rfl
map_smul' _ _ := rfl
left_inv _ := rfl
right_inv _ := rfl
