pointwise_smul_toAddSubmonoid — Mathlib

English

The toAddSubmonoid of a smul-subgroup equals the smul of the toAddSubmonoid.

Русский

Утверждение: toAddSubmonoid от подгруппы, порождённой точечным smul, совпадает с точечным smul над подмоном.

LaTeX

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

Lean4

@[simp]
theorem pointwise_smul_toAddSubmonoid (a : M) (S : AddSubgroup A) : (a • S).toAddSubmonoid = a • S.toAddSubmonoid :=
  rfl

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