Commit 2021-09-20 04:23 acb10a55

feat(linear_algebra/{multilinear,alternating): add of_subsingleton (#9196) This was refactored from the koszul_cx branch, something I mentioned doing in this Zulip thread. The original version was:

def multilinear_map.of_subsingleton (ι : Type v) [subsingleton ι] [inhabited ι] {N : Type u}
  [add_comm_group N] [module R N] (f : M →ₗ[R] N) : multilinear_map R (λ (i : ι), M) N :=
{ to_fun := λ x, f (x $ default ι),
  map_add' := λ m i x y, by rw subsingleton.elim i (default ι); simp only
    [function.update_same, f.map_add],
  map_smul' := λ m i r x, by rw subsingleton.elim i (default ι); simp only
    [function.update_same, f.map_smul], }

but I decided to remove the f : M →ₗ[R] N argument as it can be added later with (of_subsingleton R M i).comp_linear_map f.