isUnit_of_sub_one_mem_jacobson_bot

English

If r − 1 ∈ jacobson(⊥), then r is a unit.

Русский

Если r − 1 ∈ jacobson(⊥), то r является единицей.

LaTeX

$$$\text{If } r - 1 \in \operatorname{jacobson}(\bot), \text{ then } r \text{ is a unit}$$$

Lean4

theorem isUnit_of_sub_one_mem_jacobson_bot (r : R) (h : r - 1 ∈ jacobson (⊥ : Ideal R)) : IsUnit r :=
  by
  obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r h
  rw [mem_bot, sub_eq_zero, mul_comm] at hs
  exact isUnit_of_mul_eq_one _ _ hs

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