Theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_left

Modification history

2024-04-24 09:49
Mathlib/Data/Int/GCD.lean
chore: move gcd_eq_one_of_gcd_mul_right_eq_one_* earlier (#12365) …
Modified Int.gcd_eq_one_of_gcd_mul_right_eq_one_leftView on Github →
2023-03-21 13:00
Mathlib/RingTheory/Int/Basic.lean
feat: port RingTheory.Int.Basic (#3014)
Added Int.gcd_eq_one_of_gcd_mul_right_eq_one_leftView on Github →