Commit 2023-01-23 09:14 ace73592

View on Github →

feat: port Algebra.Tropical.BigOperators (#1760)

Estimated changes

added theorem Finset.trop_inf
added theorem Finset.untrop_sum'
added theorem Finset.untrop_sum
added theorem List.trop_minimum
added theorem List.trop_sum
added theorem List.untrop_prod
added theorem Multiset.trop_inf
added theorem Multiset.trop_sum
added theorem Multiset.untrop_prod
added theorem Multiset.untrop_sum
added theorem trop_infᵢ
added theorem trop_infₛ_image
added theorem trop_sum
added theorem untrop_prod
added theorem untrop_sum