coe_mul

Mathlib.NumberTheory.LucasLehmer

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

English

The map sending an integer to X_q respects multiplication: ((n * m : ℤ) : X_q) = (n : X_q) * (m : X_q).

Русский

Отображение, отправляющее целое число в X_q, сохраняет умножение: ((n * m : ℤ) : X_q) = (n : X_q) * (m : X_q).

LaTeX

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

Lean4

@[norm_cast]
theorem coe_mul (n m : ℤ) : ((n * m : ℤ) : X q) = (n : X q) * (m : X q) := by ext <;> simp

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

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

Разделы

Аффилиация

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