mathlib3 documentation

mathlib-counterexamples / linear_order_with_pos_mul_pos_eq_zero

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.

The order on foo is the one induced by the natural order on the image of aux1.

Equations

A tactic to prove facts by cases.

@[protected, instance]
Equations
theorem counterexample.foo.not_mul_pos  :
¬ {M : Type} [_inst_1 : linear_ordered_comm_monoid_with_zero M] (a b : M), 0 < a 0 < b 0 < a * b