An example of a LinearOrderedCommMonoidWithZero 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

inductive Counterexample.Foo : Type

The three element monoid.

• zero : Counterexample.Foo
• eps : Counterexample.Foo
• one : Counterexample.Foo

instance Counterexample.instDecidableEqFoo : DecidableEq Counterexample.Foo

Equations

• Counterexample.instDecidableEqFoo x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Counterexample.Foo.inhabited : Inhabited Counterexample.Foo

Equations

• Counterexample.Foo.inhabited = { default := Counterexample.Foo.zero }

instance Counterexample.Foo.instZero : Zero Counterexample.Foo

Equations

• Counterexample.Foo.instZero = { zero := Counterexample.Foo.zero }

instance Counterexample.Foo.instOne : One Counterexample.Foo

Equations

• Counterexample.Foo.instOne = { one := Counterexample.Foo.one }

def Counterexample.Foo.aux1 : Counterexample.Foo → ℕ

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

Equations

• Counterexample.Foo.zero.aux1 = 0
• Counterexample.Foo.eps.aux1 = 1
• Counterexample.Foo.one.aux1 = 2

def Counterexample.Foo.boom : Lean.ParserDescr

A tactic to prove facts by cases.

Equations

• Counterexample.Foo.boom = Lean.ParserDescr.node `Counterexample.Foo.boom 1024 (Lean.ParserDescr.nonReservedSymbol "boom" false)

theorem Counterexample.Foo.aux1_inj : Function.Injective Counterexample.Foo.aux1

instance Counterexample.Foo.linearOrder : LinearOrder Counterexample.Foo

Equations

• Counterexample.Foo.linearOrder = LinearOrder.lift' Counterexample.Foo.aux1 Counterexample.Foo.aux1_inj

def Counterexample.Foo.mul : Counterexample.Foo → Counterexample.Foo → Counterexample.Foo

Multiplication on Foo: the only external input is that ε ^ 2 = 0.

Equations

• Counterexample.Foo.one.mul x✝ = x✝
• x✝.mul Counterexample.Foo.one = x✝
• x✝¹.mul x✝ = 0

instance Counterexample.Foo.commMonoid : CommMonoid Counterexample.Foo

Equations

• Counterexample.Foo.commMonoid = CommMonoid.mk Counterexample.Foo.commMonoid.proof_6

instance Counterexample.Foo.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero Counterexample.Foo

Equations

• One or more equations did not get rendered due to their size.

theorem Counterexample.Foo.not_mul_pos : ¬∀ {M : Type} [inst : LinearOrderedCommMonoidWithZero M] (a b : M), 0 < a → 0 < b → 0 < a * b