∀ (R : Type u_2) [inst : CommRing R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (exteriorPower.alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) ∘ₗ
      have h := ⋯;
      { toFun := fun m => (exteriorPower.ιMulti R 1) fun x => m, map_add' := ⋯, map_smul' := ⋯ }) =
    LinearMap.id