mul_mem_right

Mathlib.RingTheory.Ideal.Defs

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

English

If b ∈ I, then a·b ∈ I for any a

Русский

Если b ∈ I, то a b ∈ I для любого a.

LaTeX

$$b ∈ I → a · b ∈ I$$

Lean4

theorem mul_mem_right {α} {a : α} (b : α) [Semiring α] (I : Ideal α) [I.IsTwoSided] (h : a ∈ I) : a * b ∈ I :=
  IsTwoSided.mul_mem_of_left b h

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

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

Разделы

Аффилиация

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