smul_mem — Mathlib

English

If m ∈ p and a ∈ A, then a · m ∈ p for a Submodule p of A ⊗R B acting on M.

Русский

Если m ∈ p и a ∈ A, то a · m ∈ p для p ⊆ M как подмодуля над A ⊗R B.

LaTeX

$$$$ \\forall a \\in A, \\forall m \\in p:\\ a \\cdot m \\in p. $$$$

Lean4

theorem smul_mem (p : Submodule (A ⊗[R] B) M) (a : A) {m : M} (hm : m ∈ p) : a • m ∈ p :=
  by
  suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
  simp [TensorProduct.Algebra.smul_def]

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