instNontrivial — Mathlib

English

An exterior algebra over a nontrivial ring is nontrivial; in particular, if R is nontrivial, ExteriorAlgebra_R M ≠ 0 for any M.

Русский

Алгебра внешних степеней над ненулевой кольцевой областью непустая; в частности, если R не тривиальна, то ExteriorAlgebra_R M неравна нулю для любого M.

LaTeX

$$$ \\text{Nontrivial}( \\operatorname{ExteriorAlgebra}_R M ). $$$

Lean4

/-- An `ExteriorAlgebra` over a nontrivial ring is nontrivial. -/
instance [Nontrivial R] : Nontrivial (ExteriorAlgebra R M) :=
  (algebraMap_leftInverse M).injective.nontrivial

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