rootSetFintype

Mathlib.Algebra.Polynomial.Roots

URI: https://scilib.ai/kg/mathlib#Polynomial.rootSetFintype

English

There is a finite-type instance for the root set of p in S.

Русский

Существует корректная конечная структура для множества корней p в S.

LaTeX

$$$$ \text{rootSet } p S \text{ is finite (Fintype)} $$$$

Lean4

instance rootSetFintype (p : T[X]) (S : Type*) [CommRing S] [IsDomain S] [Algebra T S] : Fintype (p.rootSet S) :=
  FinsetCoe.fintype _

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

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

Разделы

Аффилиация

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