pointwise_smul_toAddSubmonoid — Mathlib

English

The smul action preserves additive submonoids: (a · S).toAddSubmonoid = a · S.toAddSubmonoid.

Русский

Действие по точечному умножению сохраняет структуру добавочного подмоноида: (a · S).toAddSubmonoid = a · S.toAddSubmonoid.

LaTeX

$$$ (a \\cdot S).toAddSubmonoid = a \\cdot S.toAddSubmonoid $$$

Lean4

@[simp]
theorem pointwise_smul_toAddSubmonoid (a : α) (S : Submodule R M) : (a • S).toAddSubmonoid = a • S.toAddSubmonoid :=
  rfl

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