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
Equations
- Counterexample.Foo.inhabited = { default := Counterexample.Foo.zero }
Equations
- Counterexample.Foo.instZero = { zero := Counterexample.Foo.zero }
Equations
- Counterexample.Foo.instOne = { one := Counterexample.Foo.one }
A tactic to prove facts by cases.
Equations
- Counterexample.Foo.boom = Lean.ParserDescr.node `Counterexample.Foo.boom 1024 (Lean.ParserDescr.nonReservedSymbol "boom" false)
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.