one_mem_of_ne_zero_mem

Mathlib.RingTheory.SimpleRing.Basic

URI: https://scilib.ai/kg/mathlib#IsSimpleRing.one_mem_of_ne_zero_mem

Lean4

theorem one_mem_of_ne_zero_mem {A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) {x : A} (hx : x ≠ 0)
    (hxI : x ∈ I) : (1 : A) ∈ I :=
  one_mem_of_ne_bot I (by rintro rfl; exact hx hxI)

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

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

Разделы

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

Аффилиация

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