Theorem Counterexample.Foo.aux1_inj

Modification history

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