exists_mul_sub_mem_of_sub_one_mem_jacobson

Mathlib.RingTheory.Jacobson.Ideal

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

← MathLib Explorer

English

If r ∈ jac(I) with r not specified, there exists s such that s*r − 1 ∈ I.

Русский

Если r ∈ Jac(I), существует s, такой что s r − 1 ∈ I.

LaTeX

$$$\exists s, s \cdot r - 1 \in I$$$

Lean4

theorem exists_mul_sub_mem_of_sub_one_mem_jacobson {I : Ideal R} (r : R) (h : r - 1 ∈ jacobson I) :
    ∃ s, s * r - 1 ∈ I := by
  convert exists_mul_add_sub_mem_of_mem_jacobson _ h
  simp

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

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

Разделы

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

Аффилиация

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