coeffs_subset_core — Mathlib

English

Let P be an algebra presentation of an R-algebra S with generators indexed by ι and relations indexed by σ. Then every coefficient that appears among the relations lies in the core subalgebra of S, i.e. all relation coefficients belong to the core.

Русский

Пусть P — алгебраическое представление кольца над R с индексами ι для генераторов и σ для связей. Тогда все коэффициенты, встречающиеся в каких-либо отношениях, принадлежат ядру подалгебры S, т.е. коэффициенты связей лежат в ядре.

LaTeX

$$$\forall x \in \sigma,\ ((P.relation x).coeffs : Set\,R) \subseteq P.core$$$

Lean4

theorem coeffs_subset_core : P.coeffs ⊆ P.core :=
  Algebra.subset_adjoin

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