nontrivial_of_rankAtStalk_pos — Mathlib

English

Let R be a commutative ring and M an R-module. If the rank of M at the stalk is positive, then M is nontrivial (not the zero module).

Русский

Пусть R — коммутативное кольцо, M — R-модуль. Если ранг M на локализации положителен, то M не тождественно равен нулю.

LaTeX

$$$\\operatorname{rankAtStalk}(R, M) > 0 \\;\\Rightarrow\\; M \\neq 0$$$

Lean4

theorem nontrivial_of_rankAtStalk_pos (h : 0 < rankAtStalk (R := R) M) : Nontrivial M :=
  by
  by_contra! hn
  simp at h

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