adjoin_mem_finset — Mathlib

English

Under EssFiniteType, the subalgebra generated by the finite set of representatives from the finset R S equals the whole algebra S.

Русский

При условии essFiniteType подалгебра, порождаемая конечным набором элементов из σ, совпадает с всем кольцом S.

LaTeX

$$$\operatorname{adjoin}_R\{x\in S : x\in σ\} = S$$$

Lean4

theorem adjoin_mem_finset [EssFiniteType R S] : adjoin R {x : subalgebra R S | x.1 ∈ finset R S} = ⊤ :=
  adjoin_adjoin_coe_preimage

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