adjoin — Mathlib

English

adjoin_R A s denotes the smallest subalgebra of A over R that contains s (together with the image of the base field).

Русский

adjoin_R A s обозначает наименьшую подалгебру над R внутри A, содержащую множество s (вместе с образом поля-основания).

LaTeX

$$$\mathrm{adjoin}_R A(s) = \text{the smallest Subalgebra of } A \text{ over } R \text{ containing } (\operatorname{im}(\mathsf{algebraMap}\; R\; A) \cup s).$$$

Lean4

/-- The minimal subalgebra that includes `s`. -/
@[simps toSubsemiring]
def adjoin (s : Set A) : Subalgebra R A :=
  { Subsemiring.closure (Set.range (algebraMap R A) ∪ s) with
    algebraMap_mem' := fun r => Subsemiring.subset_closure <| Or.inl ⟨r, rfl⟩ }

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