IsPrimary — Mathlib

English

A proper submodule S is primary; hence S ≠ ⊤.

Русский

Всякий корректный подмодуль является примарным и поэтому не равен верхнему.м

LaTeX

$$S.IsPrimary → S ≠ ⊤$$

Lean4

/-- A proper submodule `S : Submodule R M` is primary iff
  `r • x ∈ S` implies `x ∈ S` or `∃ n : ℕ, r ^ n • (⊤ : Submodule R M) ≤ S`.
  This generalizes `Ideal.IsPrimary`. -/
protected def IsPrimary (S : Submodule R M) : Prop :=
  S ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n : ℕ, (r ^ n • ⊤ : Submodule R M) ≤ S

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