Commit 2024-02-12 00:36 66ad5718

View on Github →

feat: A natural is odd iff it's coprime with 2 (#10222) From LeanAPAP

Estimated changes

Modified Mathlib/Data/Nat/Parity.lean

Modified Mathlib/Data/Nat/Prime.lean

added theorem Nat.coprime_two_left

added theorem Nat.coprime_two_right