mem_coeffsIn

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.mem_coeffsIn

English

Membership in coeffsIn is equivalent to all coefficients belonging to M.

Русский

Членство в coeffsIn эквивалентно тому, что все коэффициенты принадлежат M.

LaTeX

$$$ p \\in coeffsIn \\iff \\forall i, p. coeff i \\in M. $$$

Lean4

theorem mem_coeffsIn : p ∈ coeffsIn σ M ↔ ∀ i, p.coeff i ∈ M :=
  .rfl

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

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

Разделы

Аффилиация

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