Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.exists_mul_mod_eq_gcd

Modification history

2021-03-30 03:44
src/data/int/gcd.lean
feat(group_theory/order_of_element): exists_pow_eq_self_of_coprime (#6875) …
Added nat.exists_mul_mod_eq_gcdView on Github →