An example of a linear_ordered_comm_monoid_with_zero in which the product of two positive
elements vanishes.
This is the monoid with 3 elements 0, ε, 1 where ε ^ 2 = 0 and everything else is forced.
The order is 0 < ε < 1. Since ε ^ 2 = 0, the product of strictly positive elements can vanish.
Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/mul_pos
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- zero : counterexample.foo
- eps : counterexample.foo
- one : counterexample.foo
The three element monoid.
Instances for counterexample.foo
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
The order on foo is the one induced by the natural order on the image of aux1.
@[protected, instance]
Multiplication on foo: the only external input is that ε ^ 2 = 0.
Equations
- 1.mul counterexample.foo.one = counterexample.foo.one
- 1.mul counterexample.foo.eps = counterexample.foo.eps
- 1.mul counterexample.foo.zero = counterexample.foo.zero
- counterexample.foo.eps.mul 1 = counterexample.foo.eps
- counterexample.foo.eps.mul counterexample.foo.eps = 0
- counterexample.foo.eps.mul counterexample.foo.zero = 0
- counterexample.foo.zero.mul 1 = counterexample.foo.zero
- counterexample.foo.zero.mul counterexample.foo.eps = 0
- counterexample.foo.zero.mul counterexample.foo.zero = 0
@[protected, instance]
Equations
- counterexample.foo.comm_monoid = {mul := counterexample.foo.mul, mul_assoc := counterexample.foo.comm_monoid._proof_1, one := 1, one_mul := counterexample.foo.comm_monoid._proof_2, mul_one := counterexample.foo.comm_monoid._proof_3, npow := monoid.npow._default 1 counterexample.foo.mul counterexample.foo.comm_monoid._proof_4 counterexample.foo.comm_monoid._proof_5, npow_zero' := counterexample.foo.comm_monoid._proof_6, npow_succ' := counterexample.foo.comm_monoid._proof_7, mul_comm := counterexample.foo.comm_monoid._proof_8}
@[protected, instance]
Equations
- counterexample.foo.linear_ordered_comm_monoid_with_zero = {le := linear_order.le counterexample.foo.linear_order, lt := linear_order.lt counterexample.foo.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le counterexample.foo.linear_order, decidable_eq := linear_order.decidable_eq counterexample.foo.linear_order, decidable_lt := linear_order.decidable_lt counterexample.foo.linear_order, max := linear_order.max counterexample.foo.linear_order, max_def := _, min := linear_order.min counterexample.foo.linear_order, min_def := _, mul := comm_monoid.mul counterexample.foo.comm_monoid, mul_assoc := _, one := comm_monoid.one counterexample.foo.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow counterexample.foo.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := counterexample.foo.linear_ordered_comm_monoid_with_zero._proof_1, zero := 0, zero_mul := counterexample.foo.linear_ordered_comm_monoid_with_zero._proof_2, mul_zero := counterexample.foo.linear_ordered_comm_monoid_with_zero._proof_3, zero_le_one := counterexample.foo.linear_ordered_comm_monoid_with_zero._proof_4}