English
The alternatization of domCoprod equals a scaled coprod with factorial factors.
Русский
Чередование domCoprod равно масштабированной копродной формы с факториалами.
LaTeX
$$$$ MultilinearMap.alternatization( (a.domCoprod b) ) = (|ιa|)! \cdot (|ιb|)! \cdot (a.domCoprod b). $$$$
Lean4
/-- If `f` is a `(n + 1)`-multilinear alternating map, `x` is an element of the domain,
and `v` is an `n`-vector, then the value of `f` at `v` with `x` inserted at the `p`th place
equals `(-1) ^ p` times the value of `f` at `v` with `x` prepended. -/
theorem map_insertNth (f : M [⋀^Fin (n + 1)]→ₗ[R] N) (p : Fin (n + 1)) (x : M) (v : Fin n → M) :
f (p.insertNth x v) = (-1) ^ (p : ℕ) • f (Matrix.vecCons x v) :=
by
rw [← cons_comp_cycleRange, map_perm, Matrix.vecCons]
simp [Units.smul_def]
