neZero_of_mem' — Mathlib

English

If IsCyclotomicExtension S A B holds, then the element n viewed in A is nonzero when n ∈ S and A is embedded accordingly.

Русский

Если IsCyclotomicExtension S A B выполняется, то образ n в A ненулевой при n ∈ S.

LaTeX

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

Lean4

theorem neZero_of_mem' [IsCyclotomicExtension S A B] [IsDomain B] (hn : n ∈ S) : NeZero (n : A) :=
  (neZero_of_mem n S A B hn).nat_of_neZero (algebraMap A B)

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