gcd_a_modEq

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.gcd_a_modEq

← MathLib Explorer

English

For natural a,b, a*gcdA(a,b) ≡ gcd(a,b) (mod b).

Русский

Для натуральных a,b имеет место a · gcdA(a,b) ≡ gcd(a,b) (mod b).

LaTeX

$$$(a : \\mathbb{Z}) \\cdot \\mathrm{gcd_A}(a,b) \\equiv \\mathrm{gcd}(a,b) [ZMOD b].$$$

Lean4

theorem gcd_a_modEq (a b : ℕ) : (a : ℤ) * Nat.gcdA a b ≡ Nat.gcd a b [ZMOD b] :=
  by
  rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
  exact (dvd_mul_right _ _).zero_modEq_int.add_left _

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

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

Разделы

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

Аффилиация

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