def omitIndex {α : Type u_1} {p : ℕ} (i : Fin (p + 1)) (vs : Fin (p + 1) → α) : Fin p → α

Given a $(p+1)$-tuple vs and an index $i$, returns the $p$-tuple obtained by omitting the $i$-th entry, used in defining the alternating expansions of forms.

def alternatingSign {p : ℕ} (i : Fin (p + 1)) : ℤ

The alternating sign $(-1)^i$ appearing in the Koszul/Cartan formulas for exterior derivative, Lie derivative, and similar antisymmetric expansions.