coe_int_mul_val_inv

Mathlib.Data.ZMod.Units

URI: https://scilib.ai/kg/mathlib#ZMod.coe_int_mul_val_inv

← MathLib Explorer

English

If gcd(m,n)=1, then m*(m^(-1) mod n) equals 1 in ZMod n.

Русский

Если gcd(m,n)=1, то m·m^(-1) по модулю n равняется 1 в ZMod n.

LaTeX

$$$$ (m \\times m^{-1}) \\equiv 1 \\pmod{n} $$$$

Lean4

theorem coe_int_mul_val_inv {n : ℕ} [NeZero n] {m : ℤ} (h : IsCoprime m n) : (m * (m⁻¹ : ZMod n).val : ZMod n) = 1 := by
  rw [natCast_zmod_val, coe_int_mul_inv_eq_one h]

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

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

Разделы

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

Аффилиация

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