mathlib
1e62218f - feat(data/int/gcd): norm_num extension for gcd (#8053)

Commit
4 years ago
feat(data/int/gcd): norm_num extension for gcd (#8053) Implements a `norm_num` plugin to evaluate terms like `nat.gcd 6 8 = 2`, `nat.coprime 127 128`, and so on for `{nat, int}.{gcd, lcm, coprime}`.
Author
Parents
Loading