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
.
fix: make an ideal lemma more constructive (#6080)
This generalizes Ideal.pow_multiset_sum_mem_span_pow
away from Classical.decEq
.