exists_supDegree_mem_support

Mathlib.Algebra.MonoidAlgebra.Degree

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.exists_supDegree_mem_support

← MathLib Explorer

English

There exists an a in the support of p such that p.supDegree D = D a.

Русский

Существует a в опоре p such that p.supDegree D = D a.

LaTeX

$$"\exists a \in p.support, p.supDegree D = D a"$$

Lean4

theorem exists_supDegree_mem_support (hp : p ≠ 0) : ∃ a ∈ p.support, p.supDegree D = D a :=
  Finset.exists_mem_eq_sup _ (Finsupp.support_nonempty_iff.mpr hp) D

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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