nontrivial — Mathlib

English

A semiring R is Nontrivial provided there exists a nontrivial module over this semiring.

Русский

Полугруппа R является ненулевой при условии существования ненулевого модуля над ней.

LaTeX

$$$\\exists M\\ [\\text{Zero } M] \\land [\\text{MulActionWithZero } R M] \\land [\\text{Nontrivial } M] \\Rightarrow \\text{Nontrivial } R$$$

Lean4

/-- A semiring is `Nontrivial` provided that there exists a nontrivial module over this semiring. -/
protected theorem nontrivial (R M : Type*) [MonoidWithZero R] [Nontrivial M] [Zero M] [MulActionWithZero R M] :
    Nontrivial R :=
  MulActionWithZero.nontrivial R M

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