Commit 2022-10-06 10:46 a87fad7b

feat(counterexamples/zero_divisors_in_add_monoid_algebras + data/finsupp/lex): add a counterexample (#16236) This PR describes a counterexample to a possible weakening of lemmas finsupp.lex.covariant_class_le_left and its analogue finsupp.lex.covariant_class_le_right: assuming only monotonicity of addition, instead of strict monotonicity would not be strong enough to prove monotonicity of addition for finsupps. See also this Zulip discussion for related material.