m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]
m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b ≡ 1 [ZMOD ↑b]
rw [← Nat.gcd_eq_gcd_ab, hgcd]
no goals
m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]
rfl