eq_top_of_unit_mem — Mathlib

English

If x ∈ I and yx = 1 for some y, then I = ⊤.

Русский

Если в идеале I есть элемент x, который имеет лево-обратную единицу, то I = ⊤.

LaTeX

$$$\\forall x,y\\\\in \\\\alpha, x\\\\in I \\\\land y x = 1 \\\\Rightarrow I = \\\\top$$$

Lean4

theorem eq_top_of_unit_mem (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤ :=
  eq_top_iff.2 fun z _ =>
    calc
      z * y * x ∈ I := I.mul_mem_left _ hx
      _ = z * (y * x) := (mul_assoc z y x)
      _ = z := by rw [h, mul_one]

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