toAddSubgroup_le — Mathlib

English

For any two submodules p and p' of M, p ≤ p' if and only if p viewed as an additive subgroup is contained in p' viewed similarly.

Русский

Для любых двух подмодулей p и p' модуля M выполняется p ≤ p' тогда и только тогда, когда p как аддитивная подгруппа содержится в p' как аддитивная подгруппа.

LaTeX

$$$p \\le p' \\iff p \\text{ (as additive subgroup)} \\le p' \\text{ (as additive subgroup)}$$$

Lean4

theorem toAddSubgroup_le : p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p' :=
  Iff.rfl

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