neZero_of_mem — Mathlib

English

If n ∈ S, then n maps to a nonzero element of B in the cyclotomic extension context.

Русский

Если n ∈ S, то образ n в B не равен нулю в контексте циклотомического расширения.

LaTeX

$$$[IsCyclotomicExtension S A B] \\;\\Rightarrow\\; (n \\in S) \\Rightarrow NeZero(n : B)$$$

Lean4

theorem neZero_of_mem [IsCyclotomicExtension S A B] [IsDomain B] (hn : n ∈ S) : NeZero (n : B) :=
  (exists_isPrimitiveRoot A B hn NeZero.out).choose_spec.neZero'

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