mem_jacobson_iff — Mathlib

English

For a two-sided ideal I in a ring R, x ∈ jacobson I if and only if a certain universal existential condition holds with respect to I.

Русский

Для двустороннего идеала I в кольце R, x ∈ jacobson(I) тогда и только тогда, когда выполняется определённое всеобщее существование над I.

LaTeX

$$x ∈ jacobson I ↔ ∀ y, ∃ z, z*y*x + z - 1 ∈ I$$

Lean4

theorem mem_jacobson_iff {x : R} {I : TwoSidedIdeal R} : x ∈ jacobson I ↔ ∀ y, ∃ z, z * y * x + z - 1 ∈ I := by
  simp [jacobson, Ideal.mem_jacobson_iff]

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