English
If two bilinear maps f and g agree on all inputs, then they are equal as bilinear maps.
Русский
Если две билинейные отображения совпадают на всех входах, то они равны как билинейные отображения.
LaTeX
$$$$ \forall m,n, f m n = g m n \Rightarrow f = g. $$$$
Lean4
/-- Create a bilinear map from a function that is semilinear in each component.
See `mk₂'` and `mk₂` for the linear case. -/
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 : S) (m n), f m (c • n) = σ₁₂ c • f m n) : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
where
toFun
m :=
{ toFun := f m
map_add' := H3 m
map_smul' := fun c => H4 c m }
map_add' m₁ m₂ := LinearMap.ext <| H1 m₁ m₂
map_smul' c m := LinearMap.ext <| H2 c m
