eq_top_of_norm_lt_one — Mathlib

English

If I is an ideal containing an element x with x ∈ I and ||1 - x|| < 1, then I = ⊤.

Русский

Если I содержит элемент x с x ∈ I и ||1 - x|| < 1, то I = ⊤.

LaTeX

$$$x \\in I \\wedge \\|1 - x\\| < 1 \\Rightarrow I = R$$$

Lean4

/-- An ideal which contains an element within `1` of `1 : R` is the unit ideal. -/
theorem eq_top_of_norm_lt_one (I : Ideal R) {x : R} (hxI : x ∈ I) (hx : ‖1 - x‖ < 1) : I = ⊤ :=
  let u := Units.oneSub (1 - x) hx
  I.eq_top_iff_one.mpr <| by simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI

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