Commit 2023-06-16 10:24 18f81f5e

View on Github →

feat: port Counterexamples.LinearOrderWithPosMulPosEqZero (#5124)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/LinearOrderWithPosMulPosEqZero.lean

added def Counterexample.Foo.aux1

added theorem Counterexample.Foo.aux1_inj

added def Counterexample.Foo.mul

added theorem Counterexample.Foo.not_mul_pos

added inductive Counterexample.Foo