pointwise_smul_toAddSubgroup — Mathlib

English

Same compatibility holds for AddSubgroups: (a · S).toAddSubgroup = a · S.toAddSubgroup.

Русский

Та же совместимость справедлива для подгрупп как AddSubgroup: (a · S).toAddSubgroup = a · S.toAddSubgroup.

LaTeX

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

Lean4

@[simp]
theorem pointwise_smul_toAddSubgroup {R M : Type*} [Ring R] [AddCommGroup M] [DistribMulAction α M] [Module R M]
    [SMulCommClass α R M] (a : α) (S : Submodule R M) : (a • S).toAddSubgroup = a • S.toAddSubgroup :=
  rfl

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