nontrivial — Mathlib

English

Let M be a simple module over a ring R. Then M is nontrivial; in particular, there exists a nonzero element whose R-span equals M.

Русский

Пусть M - простой модуль над кольцом R. Тогда M не тривиален; существует ненулевой элемент x такой, что Rx = M.

LaTeX

$$$\\text{IsSimpleModule } R\\; M \\;\\rightarrow\\; \\text{Nontrivial } M$$$

Lean4

theorem nontrivial [IsSimpleModule R M] : Nontrivial M :=
  ⟨⟨0, by
      have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
      contrapose! h
      ext x
      simp [Submodule.mem_bot, Submodule.mem_top, h x]⟩⟩

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