Commit 2023-11-03 20:42 b49464e1

feat(Counterexamples/CliffordAlgebra_not_injective): algebraMap is not always injective. (#6657) This provides a counterexample for the claim that Function.Injective (algebraMap R <| CliffordAlgebra Q). This is a formalization of https://mathoverflow.net/questions/60596/clifford-pbw-theorem-for-quadratic-form/87958[#87958](https://github.com/leanprover-community/mathlib4/pull/87958) Some Zulip discussion is at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.F0.9D.94.BD.E2.82.82.5B.CE.B1.2C.20.CE.B2.2C.20.CE.B3.5D.20.2F.20.28.CE.B1.C2.B2.2C.20.CE.B2.C2.B2.2C.20.CE.B3.C2.B2.29/near/222716333.