instNontrivialOfInvertibleOfNat — Mathlib

English

If R is nontrivial and 2 is invertible, then CliffordAlgebra Q is nontrivial.

Русский

Если R ненулевое и 2 обратимо, то CliffordAlgebra(Q) не тривиальна.

LaTeX

$$$\text{Nontrivial}(R) \Rightarrow \bigl(\mathrm{Invertible}(2) \Rightarrow \mathrm{Nontrivial}(\mathrm{CliffordAlgebra}(Q))\bigr)$$$

Lean4

/-- 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

Похожие утверждения