Zulip Chat Archive
Stream: mathlib4
Topic: Nat.two_dvd_ne_zero
Michael Stoll (Apr 19 2024 at 18:05):
Why is docs#Nat.two_dvd_ne_zero named like this? The statement is ¬ 2 ∣ n ↔ n % 2 = 1...
And it seems we are missing the converse to docs#Odd.not_two_dvd_nat.
Yaël Dillies (Apr 19 2024 at 21:33):
This is on its way to being solved. Please wait for #11863
Yaël Dillies (Apr 19 2024 at 21:34):
(or review #11986)
Last updated: May 02 2025 at 03:31 UTC