mathlib3

acb10a55 - feat(linear_algebra/{multilinear,alternating): add of_subsingleton (#9196)

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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/two.20decidable_eq.20instances.20on.20.28fin.201.29.20in.20mathlib.20.3A-.28/near/225596630). The original version was: ```lean 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`. Co-authored-by: Amelia Livingston <al3717@ic.ac.uk>