neZero'

Mathlib.NumberTheory.Cyclotomic.Basic

URI: https://scilib.ai/kg/mathlib#IsCyclotomicExtension.neZero'

English

If IsCyclotomicExtension {n} A B and B is a domain, then NeZero (n : A).

Русский

Если IsCyclotomicExtension {n} A B и B — область интеграции, то образ n в A не ноль.

LaTeX

$$$[IsCyclotomicExtension\\{n\\} A B] [IsDomain B] \\Rightarrow NeZero(n : A)$$$

Lean4

protected theorem neZero' [IsCyclotomicExtension { n } A B] [IsDomain B] : NeZero (n : A) :=
  neZero_of_mem' n { n } A B (mem_singleton n)

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

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

Разделы

Аффилиация

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