instModule — Mathlib

English

As above, for nonnegative scalars the strict ordered module structure holds.

Русский

Аналогично, для неотрицательных скаляров структура строгого упорядоченного модуля сохраняется.

LaTeX

$$$ IsStrictOrderedModule \\ R_{\\ge 0} M $$$

Lean4

/-- A module over an ordered semiring is also a module over just the non-negative scalars. -/
instance instModule : Module R≥0 M :=
  .compHom M coeRingHom

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