mem_colon' — Mathlib

English

Let N ⊆ M and P ⊆ M be submodules of a module M over a commutative semiring R. For r ∈ R, r belongs to N.colon P if and only if P ⊆ comap (r • id_M) N; equivalently, rP ⊆ N.

Русский

Пусть N ⊆ M и P ⊆ M — подмодули над кольцом R. Для элемента r ∈ R верно: r ∈ N.colon P тогда и только тогда, когда P ⊆ comap (r • id_M) N; эквивалентно, rP ⊆ N.

LaTeX

$$$ r \\in N : P \\iff P \\le \\mathrm{comap}(r \\cdot \\mathrm{id}_M)\\,N $$$

Lean4

theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N :=
  mem_colon

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