Commit 2022-10-06 10:46 a87fad7b

View on Github →

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.

Estimated changes

added theorem F.f010
added theorem F.f011
added theorem F.f110
added theorem F.f111
added theorem F.f1
added def F.val
added theorem F.z01
added def list.drop_until
added theorem single_zero_one