Commit 2023-06-17 05:17 c1430826

View on Github →

feat: port Counterexamples.CanonicallyOrderedCommSemiringTwoMul (#5162)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

added def Counterexample.ExL.L

added theorem Counterexample.ExL.add_L

added theorem Counterexample.ExL.bot_le

added theorem Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zero

added theorem Counterexample.ExL.exists_add_of_le

added def Counterexample.ExL.lSubsemiring

added theorem Counterexample.ExL.le_self_add

added theorem Counterexample.ExL.mul_L

added def Counterexample.FromBhavik.K

added theorem Counterexample.Nxzmod2.add_le_add_left

added theorem Counterexample.Nxzmod2.add_left_cancel

added theorem Counterexample.Nxzmod2.le_of_add_le_add_left

added theorem Counterexample.Nxzmod2.lt_def

added theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_left

added theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_right

added theorem Counterexample.add_self_zmod_2

added theorem Counterexample.mem_zmod_2