CliffordAlgebra.even.algHom_ext

theorem CliffordAlgebra.even.algHom_ext : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : QuadraticForm R M) {A : Type uA} [inst_3 : Ring A] [inst_4 : Algebra R A] ⦃f g : ↥(CliffordAlgebra.even Q) →ₐ[R] A⦄, (CliffordAlgebra.even.ι Q).compr₂ f = (CliffordAlgebra.even.ι Q).compr₂ g → f = g

This theorem states that for any commutative ring `R`, additively commutative group `M`, and module `M` over `R`, given a quadratic form `Q` on `M` with coefficients in `R`, and any ring `A` that is also an `R`-algebra, if we have two algebra morphisms (`f` and `g`) from the even subalgebra of the Clifford algebra of `Q` to `A` and if these two morphisms agree on pairs of generators of the even subalgebra (as expressed by the equality `(CliffordAlgebra.even.ι Q).compr₂ f = (CliffordAlgebra.even.ι Q).compr₂ g`), then the two morphisms `f` and `g` are indeed equal. The term "pairs of generators" refers to the elements obtained by the embedding of pairs of vectors into the even subalgebra, implemented as a bilinear map `CliffordAlgebra.even.ι Q`.

More concisely: Given a commutative ring `R`, additively commutative group `M` with a quadratic form `Q` and coefficients in `R`, if two algebra morphisms from the even subalgebra of the Clifford algebra of `Q` to an `R`-algebra `A` agree on pairs of generators, then they are equal.