instCharZero

Mathlib.NumberTheory.Cyclotomic.Basic

URI: https://scilib.ai/kg/mathlib#CyclotomicField.instCharZero

English

As above, X^n-1 splits over the cyclotomic field.

Русский

Как выше, X^n-1 распадается над циклотомическим полем.

LaTeX

$$$IsSplittingField(K,L,X^n-1)$$$

Lean4

instance [CharZero K] : CharZero (CyclotomicField n K) :=
  charZero_of_injective_algebraMap (algebraMap K _).injective

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

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

Разделы

Аффилиация

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