toAddSubgroup_strictMono — Mathlib

English

The map that sends a submodule p of a module M to p viewed as an additive subgroup of M is strictly increasing with respect to inclusion: if p is a proper submodule of p', then p viewed as an additive subgroup is a proper subset of p' viewed similarly.

Русский

Отображение, переводящее подмодуль p модуля M в p как подстановку в виде аддитивной подгруппы M, строго возрастает по включению: если p является proper подмодулем p', то p как аддитивная подгруппа строго включена в p'.

LaTeX

$$$p \\subsetneq p' \\Rightarrow p \\text{ (as additive subgroup)} \\subsetneq p' \\text{ (as additive subgroup)}$$$

Lean4

@[mono]
theorem toAddSubgroup_strictMono : StrictMono (toAddSubgroup : Submodule R M → AddSubgroup M) := fun _ _ => id

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