∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0),
  ((ExteriorAlgebra.lift R) ⟨f, cond⟩).toLinearMap ∘ₗ ExteriorAlgebra.ι R = f