Basic

📁 Source: Mathlib/Algebra/Tropical/Basic.lean

Statistics

Metric	Count
Definitions `Tropical`, `decidableLE`, `decidableLT`, `instAdd`, `instAddCommMonoidTropical`, `instAddCommSemigroupTropical`, `instAddMonoidWithOneTropical`, `instCommGroupOfAddCommGroup`, `instCommMonoidTropical`, `instCommSemigroupTropical`, `instCommSemiring`, `instDecidableEq`, `instDistribTropical`, `instDivOfSub`, `instGroupTropical`, `instInhabited`, `instInvOfNeg`, `instLETropical`, `instLTTropical`, `instLinearOrderTropical`, `instMonoidTropical`, `instMulOfAdd`, `instMulOneClassTropical`, `instOneTropical`, `instOrderTop`, `instPartialOrderTropical`, `instPowOfSMul`, `instPreorderTropical`, `instSemigroupTropical`, `instTopTropical`, `instZeroTropical`, `trop`, `tropEquiv`, `tropOrderIso`, `tropRec`, `untrop`	36
Theorems `addLeftMono`, `add_eq_iff`, `add_eq_left`, `add_eq_left_iff`, `add_eq_right`, `add_eq_right_iff`, `add_eq_zero_iff`, `add_pow`, `add_self`, `inf_eq_add`, `injective_trop`, `injective_untrop`, `instNoZeroDivisorsWithTop`, `instNontrivialWithTopOfZero`, `le_zero`, `leftInverse_trop`, `min_eq_add`, `mulLeftMono`, `mulLeftStrictMono`, `mulRightMono`, `mulRightStrictMono`, `mul_eq_zero_iff`, `rightInverse_trop`, `succ_nsmul`, `surjective_trop`, `surjective_untrop`, `tropEquiv_coe_fn`, `tropEquiv_symm_coe_fn`, `tropOrderIso_coe_fn`, `tropOrderIso_symm_coe_fn`, `trop_add`, `trop_add_def`, `trop_coe_ne_zero`, `trop_eq_iff_eq_untrop`, `trop_inf`, `trop_inj_iff`, `trop_injective`, `trop_max_def`, `trop_min`, `trop_monotone`, `trop_mul_def`, `trop_nsmul`, `trop_smul`, `trop_sup_def`, `trop_top`, `trop_untrop`, `trop_zero`, `trop_zsmul`, `untrop_add`, `untrop_div`, `untrop_eq_iff_eq_trop`, `untrop_inj_iff`, `untrop_injective`, `untrop_inv`, `untrop_le_iff`, `untrop_lt_iff`, `untrop_max`, `untrop_monotone`, `untrop_mul`, `untrop_one`, `untrop_pow`, `untrop_sup`, `untrop_trop`, `untrop_zero`, `untrop_zpow`, `zero_ne_trop_coe`	66
Total	102

Tropical

Definitions

Name	Category	Theorems
`decidableLE` 📖	CompOp	—
`decidableLT` 📖	CompOp	—
`instAdd` 📖	CompOp	16 math math: `min_eq_add`, `add_eq_left_iff`, `trop_min`, `add_eq_iff`, `untrop_add`, `addLeftMono`, `add_eq_zero_iff`, `add_self`, `trop_add_def`, `add_eq_right_iff`, `add_pow`, `trop_inf`, `List.trop_minimum`, `inf_eq_add`, `add_eq_right`, `add_eq_left`
`instAddCommMonoidTropical` 📖	CompOp	10 math math: `Multiset.untrop_sum`, `Multiset.trop_inf`, `untrop_sum`, `succ_nsmul`, `trop_iInf`, `Finset.untrop_sum`, `Finset.trop_inf`, `Finset.untrop_sum'`, `untrop_sum_eq_sInf_image`, `trop_sInf_image`
`instAddCommSemigroupTropical` 📖	CompOp	—
`instAddMonoidWithOneTropical` 📖	CompOp	—
`instCommGroupOfAddCommGroup` 📖	CompOp	—
`instCommMonoidTropical` 📖	CompOp	4 math math: `Multiset.untrop_prod`, `Multiset.trop_sum`, `trop_sum`, `untrop_prod`
`instCommSemigroupTropical` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDistribTropical` 📖	CompOp	—
`instDivOfSub` 📖	CompOp	1 math math: `untrop_div`
`instGroupTropical` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instInvOfNeg` 📖	CompOp	1 math math: `untrop_inv`
`instLETropical` 📖	CompOp	10 math math: `tropOrderIso_symm_coe_fn`, `mulRightMono`, `add_eq_left_iff`, `add_eq_iff`, `addLeftMono`, `le_zero`, `untrop_le_iff`, `add_eq_right_iff`, `mulLeftMono`, `tropOrderIso_coe_fn`
`instLTTropical` 📖	CompOp	3 math math: `mulRightStrictMono`, `untrop_lt_iff`, `mulLeftStrictMono`
`instLinearOrderTropical` 📖	CompOp	6 math math: `min_eq_add`, `untrop_max`, `trop_sup_def`, `trop_max_def`, `untrop_sup`, `inf_eq_add`
`instMonoidTropical` 📖	CompOp	—
`instMulOfAdd` 📖	CompOp	11 math math: `mulRightStrictMono`, `instNoZeroDivisorsWithTop`, `mulRightMono`, `mul_eq_zero_iff`, `List.trop_sum`, `untrop_mul`, `trop_add`, `trop_mul_def`, `mulLeftMono`, `List.untrop_prod`, `mulLeftStrictMono`
`instMulOneClassTropical` 📖	CompOp	—
`instOneTropical` 📖	CompOp	4 math math: `trop_zero`, `untrop_one`, `List.trop_sum`, `List.untrop_prod`
`instOrderTop` 📖	CompOp	—
`instPartialOrderTropical` 📖	CompOp	—
`instPowOfSMul` 📖	CompOp	6 math math: `untrop_pow`, `trop_smul`, `trop_nsmul`, `add_pow`, `trop_zsmul`, `untrop_zpow`
`instPreorderTropical` 📖	CompOp	2 math math: `untrop_monotone`, `trop_monotone`
`instSemigroupTropical` 📖	CompOp	—
`instTopTropical` 📖	CompOp	—
`instZeroTropical` 📖	CompOp	7 math math: `instNoZeroDivisorsWithTop`, `mul_eq_zero_iff`, `le_zero`, `add_eq_zero_iff`, `trop_top`, `untrop_zero`, `List.trop_minimum`
`trop` 📖	CompOp	33 math math: `trop_zero`, `surjective_trop`, `trop_untrop`, `tropEquiv_coe_fn`, `rightInverse_trop`, `trop_smul`, `injective_trop`, `trop_min`, `List.trop_sum`, `trop_sup_def`, `Multiset.trop_inf`, `Multiset.trop_sum`, `trop_nsmul`, `trop_max_def`, `trop_inj_iff`, `trop_add_def`, `trop_eq_iff_eq_untrop`, `trop_iInf`, `trop_add`, `Finset.trop_inf`, `trop_top`, `trop_sum`, `trop_mul_def`, `trop_zsmul`, `untrop_trop`, `trop_inf`, `trop_monotone`, `trop_sInf_image`, `tropOrderIso_coe_fn`, `trop_injective`, `List.trop_minimum`, `leftInverse_trop`, `untrop_eq_iff_eq_trop`
`tropEquiv` 📖	CompOp	2 math math: `tropEquiv_coe_fn`, `tropEquiv_symm_coe_fn`
`tropOrderIso` 📖	CompOp	2 math math: `tropOrderIso_symm_coe_fn`, `tropOrderIso_coe_fn`
`tropRec` 📖	CompOp	—
`untrop` 📖	CompOp	37 math math: `injective_untrop`, `untrop_one`, `tropOrderIso_symm_coe_fn`, `untrop_lt_iff`, `untrop_max`, `untrop_pow`, `Multiset.untrop_sum`, `trop_untrop`, `untrop_inj_iff`, `rightInverse_trop`, `surjective_untrop`, `untrop_mul`, `trop_sup_def`, `Multiset.untrop_prod`, `untrop_sum`, `untrop_add`, `tropEquiv_symm_coe_fn`, `trop_max_def`, `trop_add_def`, `trop_eq_iff_eq_untrop`, `Finset.untrop_sum`, `untrop_le_iff`, `Finset.untrop_sum'`, `untrop_monotone`, `untrop_prod`, `trop_mul_def`, `untrop_inv`, `untrop_sum_eq_sInf_image`, `untrop_div`, `untrop_trop`, `untrop_injective`, `List.untrop_prod`, `untrop_zero`, `untrop_sup`, `leftInverse_trop`, `untrop_zpow`, `untrop_eq_iff_eq_trop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `Tropical` `instAdd` `instLETropical` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_total` `add_eq_left` `LE.le.trans` `le_refl` `add_eq_right`
`add_eq_iff` 📖	mathematical	—	`Tropical` `instAdd` `instLETropical` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`trop_add_def` `trop_eq_iff_eq_untrop`
`add_eq_left` 📖	mathematical	`Tropical` `instLETropical` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`instAdd`	—	`untrop_injective`
`add_eq_left_iff` 📖	mathematical	—	`Tropical` `instAdd` `instLETropical` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`trop_add_def` `trop_eq_iff_eq_untrop` `untrop_le_iff` `min_eq_left_iff`
`add_eq_right` 📖	mathematical	`Tropical` `instLETropical` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`instAdd`	—	`untrop_injective`
`add_eq_right_iff` 📖	mathematical	—	`Tropical` `instAdd` `instLETropical` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`trop_add_def` `trop_eq_iff_eq_untrop` `untrop_le_iff` `min_eq_right_iff`
`add_eq_zero_iff` 📖	mathematical	—	`Tropical` `WithTop` `instAdd` `WithTop.linearOrder` `instZeroTropical` `WithTop.top`	—	`add_eq_iff` `le_antisymm` `le_zero`
`add_pow` 📖	mathematical	—	`Tropical` `instPowOfSMul` `AddMonoid.toNatSMul` `instAdd`	—	`le_total` `add_eq_left` `pow_le_pow_left'` `mulLeftMono` `mulRightMono` `add_eq_right`
`add_self` 📖	mathematical	—	`Tropical` `instAdd`	—	`untrop_injective` `min_eq_right` `le_rfl`
`inf_eq_add` 📖	mathematical	—	`Tropical` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderTropical` `instAdd`	—	—
`injective_trop` 📖	mathematical	—	`Tropical` `trop`	—	`Equiv.injective`
`injective_untrop` 📖	mathematical	—	`Tropical` `untrop`	—	`Equiv.injective`
`instNoZeroDivisorsWithTop` 📖	mathematical	—	`NoZeroDivisors` `Tropical` `WithTop` `instMulOfAdd` `WithTop.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instZeroTropical` `WithTop.top`	—	`mul_eq_zero_iff`
`instNontrivialWithTopOfZero` 📖	mathematical	—	`Nontrivial` `Tropical` `WithTop`	—	`trop_injective` `WithTop.top_ne_coe`
`le_zero` 📖	mathematical	—	`Tropical` `instLETropical` `instZeroTropical` `OrderTop.toTop`	—	`le_top`
`leftInverse_trop` 📖	mathematical	—	`Tropical` `trop` `untrop`	—	`trop_untrop`
`min_eq_add` 📖	mathematical	—	`Tropical` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderTropical` `instAdd`	—	—
`mulLeftMono` 📖	mathematical	—	`MulLeftMono` `Tropical` `instMulOfAdd` `instLETropical`	—	`add_le_add_right`
`mulLeftStrictMono` 📖	mathematical	—	`MulLeftStrictMono` `Tropical` `instMulOfAdd` `instLTTropical`	—	`add_lt_add_right` `untrop_lt_iff`
`mulRightMono` 📖	mathematical	—	`MulRightMono` `Tropical` `instMulOfAdd` `instLETropical`	—	`add_le_add_left`
`mulRightStrictMono` 📖	mathematical	—	`MulRightStrictMono` `Tropical` `instMulOfAdd` `instLTTropical` `Preorder.toLT`	—	`add_lt_add_left`
`mul_eq_zero_iff` 📖	mathematical	—	`Tropical` `WithTop` `instMulOfAdd` `WithTop.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instZeroTropical` `WithTop.top`	—	—
`rightInverse_trop` 📖	mathematical	—	`Tropical` `trop` `untrop`	—	`untrop_trop`
`succ_nsmul` 📖	mathematical	—	`Tropical` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `instAddCommMonoidTropical`	—	`one_nsmul` `add_nsmul` `add_self`
`surjective_trop` 📖	mathematical	—	`Tropical` `trop`	—	`Equiv.surjective`
`surjective_untrop` 📖	mathematical	—	`Tropical` `untrop`	—	`Equiv.surjective`
`tropEquiv_coe_fn` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Tropical` `EquivLike.toFunLike` `Equiv.instEquivLike` `tropEquiv` `trop`	—	—
`tropEquiv_symm_coe_fn` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Tropical` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `tropEquiv` `untrop`	—	—
`tropOrderIso_coe_fn` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Tropical` `Preorder.toLE` `instLETropical` `instFunLikeOrderIso` `tropOrderIso` `trop`	—	—
`tropOrderIso_symm_coe_fn` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Tropical` `instLETropical` `Preorder.toLE` `instFunLikeOrderIso` `OrderIso.symm` `tropOrderIso` `untrop`	—	—
`trop_add` 📖	mathematical	—	`trop` `Tropical` `instMulOfAdd`	—	—
`trop_add_def` 📖	mathematical	—	`Tropical` `instAdd` `trop` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `untrop`	—	—
`trop_coe_ne_zero` 📖	—	—	—	—	—
`trop_eq_iff_eq_untrop` 📖	mathematical	—	`trop` `untrop`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`trop_inf` 📖	mathematical	—	`trop` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Tropical` `instAdd`	—	—
`trop_inj_iff` 📖	mathematical	—	`trop`	—	—
`trop_injective` 📖	mathematical	—	`Tropical` `trop`	—	—
`trop_max_def` 📖	mathematical	—	`Tropical` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderTropical` `trop` `untrop`	—	—
`trop_min` 📖	mathematical	—	`trop` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Tropical` `instAdd`	—	—
`trop_monotone` 📖	mathematical	—	`Monotone` `Tropical` `instPreorderTropical` `trop`	—	—
`trop_mul_def` 📖	mathematical	—	`Tropical` `instMulOfAdd` `trop` `untrop`	—	—
`trop_nsmul` 📖	mathematical	—	`trop` `AddMonoid.toNatSMul` `Tropical` `instPowOfSMul`	—	—
`trop_smul` 📖	mathematical	—	`trop` `Tropical` `instPowOfSMul`	—	—
`trop_sup_def` 📖	mathematical	—	`Tropical` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderTropical` `trop` `untrop`	—	—
`trop_top` 📖	mathematical	—	`trop` `Top.top` `Tropical` `instZeroTropical`	—	—
`trop_untrop` 📖	mathematical	—	`trop` `untrop`	—	—
`trop_zero` 📖	mathematical	—	`trop` `Tropical` `instOneTropical`	—	—
`trop_zsmul` 📖	mathematical	—	`trop` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Tropical` `instPowOfSMul`	—	—
`untrop_add` 📖	mathematical	—	`untrop` `Tropical` `instAdd` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`untrop_div` 📖	mathematical	—	`untrop` `Tropical` `instDivOfSub`	—	—
`untrop_eq_iff_eq_trop` 📖	mathematical	—	`untrop` `trop`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`untrop_inj_iff` 📖	mathematical	—	`untrop`	—	—
`untrop_injective` 📖	mathematical	—	`Tropical` `untrop`	—	—
`untrop_inv` 📖	mathematical	—	`untrop` `Tropical` `instInvOfNeg`	—	—
`untrop_le_iff` 📖	mathematical	—	`untrop` `Tropical` `instLETropical`	—	—
`untrop_lt_iff` 📖	mathematical	—	`untrop` `Tropical` `instLTTropical`	—	—
`untrop_max` 📖	mathematical	—	`untrop` `Tropical` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderTropical`	—	—
`untrop_monotone` 📖	mathematical	—	`Monotone` `Tropical` `instPreorderTropical` `untrop`	—	—
`untrop_mul` 📖	mathematical	—	`untrop` `Tropical` `instMulOfAdd`	—	—
`untrop_one` 📖	mathematical	—	`untrop` `Tropical` `instOneTropical`	—	—
`untrop_pow` 📖	mathematical	—	`untrop` `Tropical` `instPowOfSMul`	—	—
`untrop_sup` 📖	mathematical	—	`untrop` `Tropical` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderTropical`	—	—
`untrop_trop` 📖	mathematical	—	`untrop` `trop`	—	—
`untrop_zero` 📖	mathematical	—	`untrop` `Tropical` `instZeroTropical` `Top.top`	—	—
`untrop_zpow` 📖	mathematical	—	`untrop` `Tropical` `instPowOfSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	—
`zero_ne_trop_coe` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`Tropical` 📖	CompOp	72 math math: `Tropical.mulRightStrictMono`, `Tropical.trop_zero`, `Tropical.injective_untrop`, `Tropical.untrop_one`, `Tropical.instNoZeroDivisorsWithTop`, `Tropical.tropOrderIso_symm_coe_fn`, `Tropical.untrop_lt_iff`, `Tropical.min_eq_add`, `Tropical.mulRightMono`, `Tropical.untrop_max`, `Tropical.untrop_pow`, `Multiset.untrop_sum`, `Tropical.surjective_trop`, `Tropical.mul_eq_zero_iff`, `Tropical.tropEquiv_coe_fn`, `Tropical.rightInverse_trop`, `Tropical.surjective_untrop`, `Tropical.trop_smul`, `Tropical.injective_trop`, `Tropical.add_eq_left_iff`, `Tropical.trop_min`, `List.trop_sum`, `Tropical.untrop_mul`, `Tropical.add_eq_iff`, `Tropical.trop_sup_def`, `Multiset.untrop_prod`, `Tropical.instNontrivialWithTopOfZero`, `Multiset.trop_inf`, `untrop_sum`, `Tropical.untrop_add`, `Tropical.succ_nsmul`, `Multiset.trop_sum`, `Tropical.tropEquiv_symm_coe_fn`, `Tropical.trop_nsmul`, `Tropical.addLeftMono`, `Tropical.trop_max_def`, `Tropical.le_zero`, `Tropical.add_eq_zero_iff`, `Tropical.add_self`, `Tropical.trop_add_def`, `trop_iInf`, `Finset.untrop_sum`, `Tropical.trop_add`, `Finset.trop_inf`, `Tropical.trop_top`, `Tropical.untrop_le_iff`, `Finset.untrop_sum'`, `trop_sum`, `Tropical.untrop_monotone`, `untrop_prod`, `Tropical.add_eq_right_iff`, `Tropical.trop_mul_def`, `Tropical.add_pow`, `Tropical.untrop_inv`, `untrop_sum_eq_sInf_image`, `Tropical.trop_zsmul`, `Tropical.untrop_div`, `Tropical.trop_inf`, `Tropical.untrop_injective`, `Tropical.mulLeftMono`, `List.untrop_prod`, `Tropical.trop_monotone`, `trop_sInf_image`, `Tropical.tropOrderIso_coe_fn`, `Tropical.untrop_zero`, `Tropical.untrop_sup`, `Tropical.trop_injective`, `Tropical.mulLeftStrictMono`, `List.trop_minimum`, `Tropical.inf_eq_add`, `Tropical.leftInverse_trop`, `Tropical.untrop_zpow`

---

← Back to Index