gcd_pow_left_dvd_pow_gcd — Mathlib

English

For any a,b and natural k, gcd(a^k, b) divides gcd(a,b)^k.

Русский

Для любых a,b и натурального k: gcd(a^k, b) делит gcd(a,b)^k.

LaTeX

$$$\\\\gcd (a^k) b \\\\mid (\\\\gcd a b)^k$$$

Lean4

theorem gcd_pow_left_dvd_pow_gcd [GCDMonoid α] {a b : α} {k : ℕ} : gcd (a ^ k) b ∣ gcd a b ^ k :=
  calc
    gcd (a ^ k) b ∣ gcd b (a ^ k) := (gcd_comm' _ _).dvd
    _ ∣ gcd b a ^ k := gcd_pow_right_dvd_pow_gcd
    _ ∣ gcd a b ^ k := pow_dvd_pow_of_dvd (gcd_comm' _ _).dvd _

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