smul_mem' — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\forall b \\in B, \\forall m \\in p:\\ b \\cdot m \\in p. $$$$

Lean4

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

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