smul_le_smul — Mathlib

English

If s ⊆ t as SetSemirings and M ≤ N, then s • M ≤ t • N in the Submodule lattice.

Русский

Если s ⊆ t как SetSemiring и M ≤ N, тогда s • M ≤ t • N в решётке подмодулей.

LaTeX

$$$\text{If } h_1: \ Down(s) \subseteq Down(t) \text{ and } h_2: M \le N,\; s \cdot M \le t \cdot N.$$$

Lean4

theorem smul_le_smul {s t : SetSemiring A} {M N : Submodule R A}
    (h₁ : SetSemiring.down (α := A) s ⊆ SetSemiring.down (α := A) t) (h₂ : M ≤ N) : s • M ≤ t • N :=
  mul_le_mul' (span_mono h₁) h₂

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