instNontrivialOfFactLtNatOfNat

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.X.instNontrivialOfFactLtNatOfNat

English

If q > 1, then X_q is a nontrivial algebraic object (there exist two distinct elements in X_q).

Русский

Пусть q > 1. Тогда X_q не тождественно нулевая структура (существуют две различные элементы в X_q).

LaTeX

$$$ \exists x,y \in X_q\; (x \neq y) $$$

Lean4

instance [Fact (1 < (q : ℕ))] : Nontrivial (X q) :=
  ⟨⟨0, 1, ne_of_apply_ne Prod.fst zero_ne_one⟩⟩

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

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

Разделы

Аффилиация

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