ω_mul_ωb

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.X.ω_mul_ωb

English

ω and ω_b are multiplicative inverses: ω · ω_b = 1.

Русский

ω и ω_b являются взаимно обратными: ω · ω_b = 1.

LaTeX

$$$ (\omega : X q) \cdot \omega_b = 1 $$$

Lean4

theorem ω_mul_ωb : (ω : X q) * ωb = 1 := by
  dsimp [ω, ωb]
  ext <;> simp; ring

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

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

Разделы

Аффилиация

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