mul_mem_left

Mathlib.RingTheory.TwoSidedIdeal.Basic

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.mul_mem_left

English

If y ∈ I, then for any x ∈ R, x·y ∈ I.

Русский

Если y ∈ I, то для любого x ∈ R выполняется x·y ∈ I.

LaTeX

$$$y \in I \Rightarrow xy \in I \text{ for all } x \in R$$$

Lean4

theorem mul_mem_left (x y) (hy : y ∈ I) : x * y ∈ I := by simpa using I.ringCon.mul (I.ringCon.refl x) hy

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

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

Разделы

Аффилиация

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