mem_set_smul_of_mem_mem — Mathlib

English

If r ∈ s and m ∈ N, then r • m ∈ s • N; i.e., smul by an element of s sends an element of N into s • N.

Русский

Если r ∈ s и m ∈ N, то r • m ∈ s • N; т.е. умножение элемента подмодуля Smul отправляет элемент в s • N.

LaTeX

$$$r \\in s \\land m \\in N \\Rightarrow r \\cdot m \\in s \\cdot N$$$

Lean4

@[aesop safe]
theorem mem_set_smul_of_mem_mem {r : S} {m : M} (mem1 : r ∈ s) (mem2 : m ∈ N) : r • m ∈ s • N :=
  by
  rw [mem_set_smul_def, mem_sInf]
  exact fun _ h => h mem1 mem2

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