feat: Nontrivial instances for ExteriorAlgebra, CliffordAlgebra (#7985)

Using methods suggested by @eric-wieser [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Nontrivial.20algebras)
leanprover-community · Oct 27, 2023 · b0a73d4 · b0a73d4
1 parent b65c6a3
commit b0a73d4
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
@@ -399,4 +399,8 @@ def equivExterior [Invertible (2 : R)] : CliffordAlgebra Q ≃ₗ[R] ExteriorAlg
   changeFormEquiv changeForm.associated_neg_proof
 #align clifford_algebra.equiv_exterior CliffordAlgebra.equivExterior
 
+/-- A `CliffordAlgebra` over a nontrivial ring is nontrivial, in characteristic not two. -/
+instance [Nontrivial R] [Invertible (2 : R)] :
+    Nontrivial (CliffordAlgebra Q) := (equivExterior Q).symm.injective.nontrivial
+
 end CliffordAlgebra
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -333,6 +333,10 @@ theorem ιMulti_succ_curryLeft {n : ℕ} (m : M) :
       rfl
 #align exterior_algebra.ι_multi_succ_curry_left ExteriorAlgebra.ιMulti_succ_curryLeft
 
+/-- An `ExteriorAlgebra` over a nontrivial ring is nontrivial. -/
+instance [Nontrivial R] : Nontrivial (ExteriorAlgebra R M) :=
+  (algebraMap_leftInverse M).injective.nontrivial
+
 end ExteriorAlgebra
 
 namespace TensorAlgebra