adjoin_le_algebra_adjoin — Mathlib

English

For a commutative semiring R, a ring A with R-algebra structure and a subset s ⊆ A, the NonUnitalAlgebra generated by s is contained in the NonUnitalSubalgebra underlying Algebra.adjoin R s; i.e., adjoin_R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra.

Русский

Для коммутативного полусоединения R, кольца A с структурой R-алгебры и подмножествa s ⊆ A, порожденный NonUnitalAlgebra генератор s вложен в NonUnitalSubalgebra, соответствующий Algebra.adjoin R s; то есть adjoin_R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra.

LaTeX

$$$ \operatorname{adjoin}_{R} s \le \bigl(\operatorname{Algebra.adjoin}_{R} s\bigr).\mathrm{toNonUnitalSubalgebra} $$$

Lean4

theorem adjoin_le_algebra_adjoin (s : Set A) : adjoin R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra :=
  adjoin_le Algebra.subset_adjoin

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