eq_top_of_isUnit_mem

Mathlib.RingTheory.Ideal.Lattice

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

English

If an element x ∈ I is a unit, then I = ⊤.

Русский

Если в идеале I элемент x является единицей, то I = ⊤.

LaTeX

$$$ \\forall x \\in I, IsUnit(x) \\\\Rightarrow I = \\\\top $$$

Lean4

theorem eq_top_of_isUnit_mem {x} (hx : x ∈ I) (h : IsUnit x) : I = ⊤ :=
  let ⟨y, hy⟩ := h.exists_left_inv
  eq_top_of_unit_mem I x y hx hy

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

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

Разделы

Аффилиация

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