essFiniteType_iff — Mathlib

English

EssFiniteType R S is equivalent to the existence, for σ, of a family of units t in Adjoin(R,σ) such that for every s ∈ S, s t lies in Adjoin(R,σ).

Русский

EssFiniteType R S эквивалентна существованию σ и семейства единиц t в Adjoin(R,σ), таких что для каждого s ∈ S выполнено s t ∈ Adjoin(R,σ).

LaTeX

$$Iff (Algebra.EssFiniteType R S) (Exists σ, IsLocalization (…))$$

Lean4

theorem essFiniteType_iff :
    EssFiniteType R S ↔
      ∃ (σ : Finset S),
        (∀ s : S, ∃ t ∈ Algebra.adjoin R (σ : Set S), IsUnit t ∧ s * t ∈ Algebra.adjoin R (σ : Set S)) :=
  by
  simp_rw [← essFiniteType_cond_iff]
  constructor <;> exact fun ⟨a, b⟩ ↦ ⟨a, b⟩

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