Mathlib Map

Theorems · Definition · algebraic geometry

Tropical

Type u → Type u

The tropicalization of a type R.

Defined in
Mathlib.Algebra.Tropical.Basic
Cited by
74 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Tropical.untrop · cited by 40Tropical.untropTropical.trop · cited by 35Tropical.tropTropical.tropEquiv · cited by 8Tropical.tropEquivTropical.trop_add_def · cited by 3Tropical.trop_add_defTropical.trop_eq_iff_eq_untrop · cited by 3Tropical.trop_eq_iff_eq_u…Tropical.untrop_injective · cited by 3Tropical.untrop_injectiveTropical.tropOrderIso · cited by 2Tropical.tropOrderIsoTropical.untrop_le_iff · cited by 2Tropical.untrop_le_iffTropical.add_eq_iff · cited by 1Tropical.add_eq_iffTropical.add_eq_left · cited by 1Tropical.add_eq_leftTropical.add_eq_right · cited by 1Tropical.add_eq_rightTropical.add_self · cited by 1Tropical.add_selftrop_sInf_image · cited by 1trop_sInf_imageMultiset.trop_inf · cited by 1Multiset.trop_infMultiset.trop_sum · cited by 1Multiset.trop_sumTropicalCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by79

Results whose statement or proof uses this declaration.