Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.exists_mul_mod_eq_one_of_coprime

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_one_of_coprimeView on Github →