Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Nxzmod_2.zero_le_one

Modification history

2022-06-06 18:41

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

feat(algebra/order/*): typeclass for `0 ≤ 1` (#14510) …

Deleted Nxzmod_2.zero_le_one View on Github →

2021-05-15 21:20

src/counterexamples/canonically_ordered_comm_semiring_two_mul.lean

feat(counterexamples/*): add counterexamples folder (#7558) …

Added Nxzmod_2.zero_le_one View on Github →