Theorem Counterexample.Foo.not_mul_pos

Modification history

2026-01-08 11:26
Counterexamples/LinearOrderWithPosMulPosEqZero.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Deleted Counterexample.Foo.not_mul_posView on Github →
2023-06-16 10:24
Counterexamples/LinearOrderWithPosMulPosEqZero.lean
feat: port Counterexamples.LinearOrderWithPosMulPosEqZero (#5124)
Added Counterexample.Foo.not_mul_posView on Github →