toAddSubmonoid_le — Mathlib

English

The order relation between submodules is equivalent to the order relation between their underlying additive submonoids.

Русский

Порядковое отношение между подпространствами эквивалентно порядковому отношению между их базовыми аддитивными подсобствами.

LaTeX

$$$p \le q \iff p.toAddSubmonoid \le q.toAddSubmonoid$$$

Lean4

theorem toAddSubmonoid_le : p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q :=
  Iff.rfl

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