basic): golf results about bUnion (#17501)

Commit

3 years ago

chore(algebra/big_operators/basic): golf results about bUnion (#17501) While the diff adds lines overall, these are new lemmas that were previously missing.

Author

eric-wieser

Parents

347d2ed1

mathlib3 62ec8656 - chore(algebra/big_operators/basic): golf results about bUnion (#17501)

mathlib3
62ec8656 - chore(algebra/big_operators/basic): golf results about bUnion (#17501)