mathlib3

a87fad7b - feat(counterexamples/zero_divisors_in_add_monoid_algebras + data/finsupp/lex): add a counterexample (#16236)

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 `finsupp`s. See also [this Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2316157.20no-zero-divisors.20in.20add_monoid_algebras) for related material.