Theorem Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zero

Modification history

2023-06-17 05:17
Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean
feat: port Counterexamples.CanonicallyOrderedCommSemiringTwoMul (#5162)
Added Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zeroView on Github →