splits_C

Mathlib.Algebra.Polynomial.Splits

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

English

Splits i (C a) holds for any a.

Русский

Splits i (C a) выполняется для любого a.

LaTeX

$$Splits i (C a) = Splits i (RingHom.instFunLike.coe Polynomial.C a)$$

Lean4

@[simp]
theorem splits_C (a : K) : Splits i (C a) :=
  splits_of_map_eq_C i (map_C i)

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

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

Разделы

Аффилиация

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