# mathlib3documentation

mathlib-counterexamples / canonically_ordered_comm_semiring_two_mul

A canonically_ordered_comm_semiring with two different elements a and b such that a ≠ b and 2 * a = 2 * b. Thus, multiplication by a fixed non-zero element of a canonically ordered semiring need not be injective. In particular, multiplying by a strictly positive element need not be strictly monotone.

Recall that a canonically_ordered_comm_semiring is a commutative semiring with a partial ordering that is "canonical" in the sense that the inequality a ≤ b holds if and only if there is a c such that a + c = b. There are several compatibility conditions among addition/multiplication and the order relation. The point of the counterexample is to show that monotonicity of multiplication cannot be strengthened to strict monotonicity.

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Bhavik Mehta's example. There are only the initial definitions, but no proofs. The Type K is a canonically ordered commutative semiring with the property that 2 * (1/2) ≤ 2 * 1, even though it is not true that 1/2 ≤ 1, since 1/2 and 1 are not comparable.

Equations
Instances for counterexample.from_Bhavik.K
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem counterexample.mem_zmod_2 (a : zmod 2) :
a = 0 a = 1
theorem counterexample.add_self_zmod_2 (a : zmod 2) :
a + a = 0
@[protected, instance]

The preorder relation on ℕ × ℤ/2ℤ where we only compare the first coordinate, except that we leave incomparable each pair of elements with the same first component. For instance, ∀ α, β ∈ ℤ/2ℤ, the inequality (1,α) ≤ (2,β) holds, whereas, ∀ n ∈ ℤ, the elements (n,0) and (n,1) are incomparable.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem counterexample.Nxzmod_2.lt_def {a b : × zmod 2} :
a < b a.fst < b.fst

A strict inequality forces the first components to be different.

theorem counterexample.Nxzmod_2.add_left_cancel (a b c : × zmod 2) :
a + b = a + c b = c
a b (c : × zmod 2), c + a c + b
@[protected, instance]
Equations
theorem counterexample.Nxzmod_2.mul_lt_mul_of_pos_left (a b c : × zmod 2) :
a < b 0 < c c * a < c * b
theorem counterexample.Nxzmod_2.mul_lt_mul_of_pos_right (a b c : × zmod 2) :
a < b 0 < c a * c < b * c
@[protected, instance]
Equations

Initially, L was defined as the subsemiring closure of (1,0).

Equations
Instances for counterexample.ex_L.L
theorem counterexample.ex_L.add_L {a b : × zmod 2} (ha : a (0, 1)) (hb : b (0, 1)) :
a + b (0, 1)
theorem counterexample.ex_L.mul_L {a b : × zmod 2} (ha : a (0, 1)) (hb : b (0, 1)) :
a * b (0, 1)

The subsemiring corresponding to the elements of L, used to transfer instances.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations