coeffs_subset_range

Mathlib.RingTheory.Extension.Presentation.Core

URI: https://scilib.ai/kg/mathlib#Algebra.Presentation.coeffs_subset_range

English

The set of coefficients of P lies inside the range of the base scalar map from R0 to R.

Русский

Множество коэффициентов P лежит в образе скалярного отображения от R0 в R.

LaTeX

$$$(P.coeffs : \\mathrm{Set}\\,R) \\subseteq \\mathrm{Set.range}(\\mathrm{algebraMap}\\,R_0\\,R)$$$

Lean4

theorem coeffs_subset_range : (P.coeffs : Set R) ⊆ Set.range (algebraMap R₀ R) :=
  HasCoeffs.coeffs_subset_range

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru