pointwise_smul_toAddSubgroup — Mathlib

English

For a surjective smul map, a•S equals a•S.toAddSubgroup.

Русский

При сюръективном отображении smul, a•S = a•S.toAddSubgroup.

LaTeX

$$$(a\cdot S)^{\text{toAddSubgroup}} = a\cdot (S^{\text{toAddSubgroup}})$$$

Lean4

@[simp]
theorem pointwise_smul_toAddSubgroup {R : Type*} [Ring R] [MulSemiringAction M R] (a : M) (S : Ideal R)
    (ha : Function.Surjective fun r : R => a • r) : (a • S).toAddSubgroup = a • S.toAddSubgroup :=
  by
  ext
  exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

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