∀ (R : Type u) [inst : CommRing R] (ι : Type u_4) [inst_1 : DecidableEq ι] (M : Type u_5) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (x : exteriorPower.presentation.Rels R ι M),
  (exteriorPower.presentation.relations R ι M).relation x =
    match x with
    | exteriorPower.presentation.Rels.add m i x y =>
      ((fun₀ | Function.update m i x => 1) + fun₀ | Function.update m i y => 1) -
        fun₀ | Function.update m i (x + y) => 1
    | exteriorPower.presentation.Rels.smul m i r x =>
      (fun₀ | Function.update m i (r • x) => 1) - r • fun₀ | Function.update m i x => 1
    | exteriorPower.presentation.Rels.alt m i j hm hij => fun₀ | m => 1