English
The coercion of an alternating map’s alternatization equals the corresponding AddMonoidHom coercion of the same map’s alternatization.
Русский
Приведение к коэффициентам алтернатизации равно соответствующему коэрцированию AddMonoidHom для той же карты.
LaTeX
$$$\\uparrow(MultilinearMap.alternatization m) = (\\text{MultilinearMap.alternatization } m)$$$
Lean4
/-- Alternatizing a multilinear map that is already alternating results in a scale factor of `n!`,
where `n` is the number of inputs. -/
theorem coe_alternatization [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') :
MultilinearMap.alternatization (a : MultilinearMap R (fun _ => M) N') = Nat.factorial (Fintype.card ι) • a :=
by
apply AlternatingMap.coe_injective
simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul, smul_smul,
Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm, ← coe_multilinearMap, coe_smul]
