ExteriorAlgebra.lhom_ext

theorem ExteriorAlgebra.lhom_ext : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] ⦃f g : ExteriorAlgebra R M →ₗ[R] N⦄, (∀ (i : ℕ), f.compAlternatingMap (ExteriorAlgebra.ιMulti R i) = g.compAlternatingMap (ExteriorAlgebra.ιMulti R i)) → f = g

This theorem states that to prove the equality of two linear maps (`f` and `g`) from the exterior algebra of an `R`-module `M` to another `R`-module `N`, it is enough to demonstrate that these maps agree on the exterior powers of `M`. This is proven by showing that the composition of `f` and `g` with the same alternating map, generated by applying the canonical injection of `M` into the exterior algebra, produces identical results for all natural numbers `i`.

More concisely: To prove the equality of two linear maps between exterior algebras of R-modules, it is sufficient to show they agree on the exterior powers.