smul_mem_pointwise_smul

Mathlib.RingTheory.Ideal.Pointwise

URI: https://scilib.ai/kg/mathlib#Ideal.smul_mem_pointwise_smul

English

If r ∈ S, then m•r ∈ m•S for any m in M, under the pointwise action on ideals.

Русский

Если r ∈ S, тогда m•r ∈ m•S для любого m∈M при покроковом действии на идеалы.

LaTeX

$$$r\in S\Rightarrow m\cdot r\in m\cdot S$$$

Lean4

theorem smul_mem_pointwise_smul (m : M) (r : R) (S : Ideal R) : r ∈ S → m • r ∈ m • S := fun h =>
  subset_span <| Set.smul_mem_smul_set h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru