exists_mul_add_sub_mem_of_mem_jacobson

Mathlib.RingTheory.Jacobson.Ideal

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

← MathLib Explorer

English

If x ∈ jac(I), then there exists s with s*(r+1) − 1 ∈ I for r = x.

Русский

Если x ∈ Jac(I), то существует s such that s*(x+1) − 1 ∈ I.

LaTeX

$$$\exists s, s \cdot (r + 1) - 1 \in I$$$

Lean4

theorem exists_mul_add_sub_mem_of_mem_jacobson {I : Ideal R} (r : R) (h : r ∈ jacobson I) : ∃ s, s * (r + 1) - 1 ∈ I :=
  by
  obtain ⟨s, hs⟩ := mem_jacobson_iff.1 h 1
  use s
  rw [mul_add, mul_one]
  simpa using hs

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

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

Разделы

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

Аффилиация

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