pow_sub_one_gcd_pow_sub_one — Mathlib

English

For natural a,b,c, gcd(a^b − 1, a^c − 1) = a^{gcd(b,c)} − 1.

Русский

Пусть a,b,c ∈ ℕ. Тогда gcd(a^b − 1, a^c − 1) = a^{gcd(b,c)} − 1.

LaTeX

$$$\gcd(a^b - 1, a^c - 1) = a^{\gcd(b,c)} - 1.$$$

Lean4

@[simp]
theorem pow_sub_one_gcd_pow_sub_one (a b c : ℕ) : gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1 :=
  by
  rcases eq_zero_or_pos b with rfl | hb
  · simp
  replace hb : c % b < b := mod_lt c hb
  rw [gcd_rec, pow_sub_one_mod_pow_sub_one, pow_sub_one_gcd_pow_sub_one, ← gcd_rec]

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