exists_inv — Mathlib

English

If I is a maximal ideal and x ∉ I, there exist y ∈ α and i ∈ I with yx + i = 1.

Русский

Если I — максимальный идеал и x ∉ I, существуют y ∈ α и i ∈ I такие, что yx + i = 1.

LaTeX

$$$I.IsMaximal \Rightarrow \forall x( x \notin I) \exists y\in α\, \exists i\in I,\ yx + i = 1$$$

Lean4

theorem exists_inv {I : Ideal α} (hI : I.IsMaximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1 :=
  by
  obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI
  rcases
    mem_span_insert.1
      (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
        (subset_span (mem_insert _ _))) with
    ⟨y, z, hz, hy⟩
  refine ⟨y, z, ?_, hy.symm⟩
  rwa [← span_eq I]

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