Commit 2025-03-13 06:05 499a8c9d
View on Github →feat(Data/Nat/GCD/Basic): Prove gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1 (#22889)
This PR proves gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1 for all a b c : ℕ.
feat(Data/Nat/GCD/Basic): Prove gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1 (#22889)
This PR proves gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1 for all a b c : ℕ.