∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  (∃ g, g ∘ₗ f = LinearMap.id) → Function.Injective ⇑(ExteriorAlgebra.map f)