mem_jacobson_bot — Mathlib

English

An element x lies in jacobson(⊥) iff for all y, x y + 1 is a unit.

Русский

Элемент x принадлежит jacobson(⊥) тогда и только тогда, когда для всех y, x y + 1 — единица.

LaTeX

$$$x \in \operatorname{jacobson}(\bot) \iff \forall y, \ IsUnit(x \cdot y + 1)$$$

Lean4

theorem mem_jacobson_bot {x : R} : x ∈ jacobson (⊥ : Ideal R) ↔ ∀ y, IsUnit (x * y + 1) :=
  ⟨fun hx y =>
    let ⟨z, hz⟩ := (mem_jacobson_iff.1 hx) y
    isUnit_iff_exists_inv.2 ⟨z, by rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]⟩,
    fun h =>
    mem_jacobson_iff.mpr fun y =>
      let ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (h y)
      ⟨b, (Submodule.mem_bot R).2 (hb ▸ by ring)⟩⟩

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