Theorems · Theorem · algebraic geometry
trop_sum
∀ {R : Type u_1} {S : Type u_2} [inst : AddCommMonoid R] (s : Finset S) (f : S → R),
Tropical.trop (∑ i ∈ s, f i) = ∏ i ∈ s, Tropical.trop (f i)- Defined in
- Mathlib.Algebra.Tropical.BigOperators
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- Finset.prodstatement and proof · cited by 2,356
- Multiset.mapproof · cited by 876
- Multiset.prodproof · cited by 528
- Finset.valproof · cited by 438
- Multiset.sumproof · cited by 388
- Multiset.map_congrproof · cited by 232
- Multiset.map_mapproof · cited by 151
- Tropicalstatement and proof · cited by 74
- Tropical.tropstatement and proof · cited by 35
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.