Commit 2023-05-16 00:56 c0f7bfde

View on Github →

feat: porting norm_num extensions for Nat.gcd, Nat.lcm, Int.gcd, Int.lcm, and IsCoprime (#3923) This completes the porting of these norm_num extensions while adding a new extension for IsCoprime over Int. It also adds the norm_num extension testing file from mathlib3. Closes #3246.

Estimated changes

added theorem Int.gcd_def
modified theorem Nat.isCoprime_iff_coprime
added theorem ex11
added theorem ex12
added theorem ex13
added theorem ex14
added theorem ex15
added theorem ex16'
added theorem ex16
added theorem ex17
added theorem ex21
added theorem ex22
added theorem ex23
added theorem ex24
added theorem ex25
added theorem ex26
added theorem ex27
added theorem ex31
added theorem ex32
added theorem ex33
added theorem ex34
added theorem ex35
added theorem ex36
added theorem ex37
added theorem ex41
added theorem ex42
added theorem ex43
added theorem ex44
added theorem ex51
added theorem ex52
added theorem ex53
added theorem ex54
added theorem ex61
added theorem ex62'
added theorem ex62
added theorem ex63
added theorem ex64