single_mem_pi

Mathlib.RingTheory.Ideal.Basic

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

← MathLib Explorer

English

If r ∈ I_i, then the Pi.single i r lies in pi I.

Русский

Если r ∈ I_i, то Pi.single i r ∈ pi I.

LaTeX

$$$\\text{If } r \\in I_i, \\; \\Pi\\text{-single}_i(r) \\in \\operatorname{pi} I$$$

Lean4

theorem single_mem_pi [DecidableEq ι] {i : ι} {r : R i} (hr : r ∈ I i) : Pi.single i r ∈ pi I :=
  by
  intro j
  obtain rfl | ne := eq_or_ne i j
  · simpa
  · simp [ne]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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