Commit 2023-09-12 22:27 aa8559ba

View on Github →

feat: gcd and coprime sub (#7051)

Estimated changes

Modified Mathlib/Data/Nat/GCD/Basic.lean

added theorem Nat.coprime_self_sub_left

added theorem Nat.coprime_self_sub_right

added theorem Nat.coprime_sub_self_left

added theorem Nat.coprime_sub_self_right

added theorem Nat.gcd_self_sub_left

added theorem Nat.gcd_self_sub_right

added theorem Nat.gcd_sub_self_left

added theorem Nat.gcd_sub_self_right