Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-15 21:20 d338ebd4

View on Github →

feat(counterexamples/*): add counterexamples folder (#7558) Several times, there has been a discussion on Zulip about the appropriateness of having counterexamples in mathlib. This PR introduces a counterexamples folder, together with the first couple of counterexamples. For the most recent discussion, see https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.237553

Estimated changes

Created src/counterexamples/canonically_ordered_comm_semiring_two_mul.lean

added theorem Nxzmod_2.add_le_add_left

added theorem Nxzmod_2.add_left_cancel

added theorem Nxzmod_2.le_of_add_le_add_left

added theorem Nxzmod_2.lt_def

added theorem Nxzmod_2.mul_lt_mul_of_pos_left

added theorem Nxzmod_2.mul_lt_mul_of_pos_right

added theorem Nxzmod_2.zero_le_one

added theorem add_self_zmod_2

added def ex_L.L

added theorem ex_L.add_L

added theorem ex_L.bot_le

added theorem ex_L.eq_zero_or_eq_zero_of_mul_eq_zero

added theorem ex_L.le_iff_exists_add

added theorem ex_L.lt_of_add_lt_add_left

added theorem ex_L.mul_L

added def from_Bhavik.K

added theorem mem_zmod_2

Created src/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean

added def foo.aux1

added theorem foo.aux1_inj

added def foo.mul

added theorem foo.not_mul_pos

added inductive foo