English
The cartesian product of two alternating maps is again alternating, with values in the product codomain; for inputs v, (f prod g)(v) = (f(v), g(v)).
Русский
Произведение двух чередующихся отображений снова чередующее отображение, значения которого лежат в произведении кардинал; для аргумента v: (f prod g)(v) = (f(v), g(v)).
LaTeX
$$$(f \mathrm{prod} g)(v) = (f(v), g(v)) \quad\text{for all } v.$$$
Lean4
/-- The Cartesian product of two alternating maps, as an alternating map. -/
@[simps!]
def prod (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) : M [⋀^ι]→ₗ[R] (N × P) :=
{ f.toMultilinearMap.prod g.toMultilinearMap with
map_eq_zero_of_eq' := fun _ _ _ h hne => Prod.ext (f.map_eq_zero_of_eq _ h hne) (g.map_eq_zero_of_eq _ h hne) }
