one_mem_nthRootsFinset

Mathlib.Algebra.Polynomial.Roots

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

English

If 0 < n, then 1 is in nthRootsFinset n 1

Русский

Если 0 < n, то 1 принадлежит nthRootsFinset n 1.

LaTeX

$$$0 < n \Rightarrow 1 \in \operatorname{nthRootsFinset}(n, 1)$$$

Lean4

theorem one_mem_nthRootsFinset (hn : 0 < n) : 1 ∈ nthRootsFinset n (1 : R) := by rw [mem_nthRootsFinset hn, one_pow]

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

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

Разделы

Аффилиация

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