Commit 2023-07-25 16:52 3bece34d

View on Github →

fix: make an ideal lemma more constructive (#6080) This generalizes Ideal.pow_multiset_sum_mem_span_pow away from Classical.decEq.

Estimated changes