instCharP

Mathlib.NumberTheory.LucasLehmer

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

← MathLib Explorer

English

((n : ℤ) : X_q) = (n : X_q) for all integers n.

Русский

Для всех целых n выполняется ((n : ℤ) : X_q) = (n : X_q).

LaTeX

$$$ ((n : \mathbb{Z}) : X q) = (n : X q) $$$

Lean4

instance : CharP (X q) q where
  cast_eq_zero_iff
    x := by
    convert ZMod.natCast_eq_zero_iff _ _
    exact ⟨congr_arg Prod.fst, fun hx ↦ ext hx (by simp)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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