coeffs_relation_subset_core — Mathlib

English

For every relation x in σ, the coefficients of the polynomial P.relation x are contained in the core subalgebra of S.

Русский

Для каждого отношения x ∈ σ коэффициенты полинома P.relation x лежат в ядре подалгебры S.

LaTeX

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

Lean4

theorem coeffs_relation_subset_core (x : σ) : ((P.relation x).coeffs : Set R) ⊆ P.core :=
  subset_trans (P.coeffs_relation_subset_coeffs x) P.coeffs_subset_core

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