exists_inv — Mathlib

English

Given a maximal ideal I, and any nonzero element a in R/I, there exists an inverse b with a·b = 1 in R/I.

Русский

Для максимального идеала I и любого ненулевого элемента a в R/I существует обратный b, такой что a·b = 1.

LaTeX

$$Exists_inv [hI : I.IsMaximal] : ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b : R ⧸ I, a * b = 1$$

Lean4

theorem exists_inv [hI : I.IsMaximal] : ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b : R ⧸ I, a * b = 1 :=
  by
  apply exists_right_inv_of_exists_left_inv
  rintro ⟨a⟩ h
  rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
  refine ⟨mk _ b, Quot.sound ?_⟩
  simp only [Submodule.quotientRel_def]
  rw [← eq_sub_iff_add_eq'] at abc
  rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc

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