ωb_mul_ω

Mathlib.NumberTheory.LucasLehmer

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

English

ω_b is the multiplicative inverse of ω, so ω_b · ω = 1.

Русский

ω_b является обратным к ω, поэтому ω_b · ω = 1.

LaTeX

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

Lean4

theorem ωb_mul_ω : (ωb : X q) * ω = 1 := by rw [mul_comm, ω_mul_ωb]

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

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

Разделы

Аффилиация

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