ωUnit

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.ωUnit

← MathLib Explorer

English

ωUnit(p) is a unit in X(q p) with specified components.

Русский

ωUnit(p) является единицей в X(q p) с заданными компонентами.

LaTeX

$$$\omegaUnit(p) \in (X (q p))^{\times}$$$

Lean4

/-- `ω` as an element of the group of units. -/
def ωUnit (p : ℕ) : Units (X (q p)) where
  val := ω
  inv := ωb
  val_inv := ω_mul_ωb
  inv_val := ωb_mul_ω

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

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

Разделы

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

Аффилиация

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