English
Let R be an additive group. Then Tropical R carries a group structure with the tropical product, i.e., Tropical R is a group under the tropical multiplication with the tropical inverse given by the untrop map.
Русский
Пусть R — аддитивная группа. Тогда у Tropical R имеется групповая структура под тропическим умножением; Tropical R образует группу относительно тропического умножения, инверсией служит отображение untrop.
LaTeX
$$$\mathrm{Tropical}(R)$ has a group structure under the tropical product.$$
Lean4
instance instGroupTropical [AddGroup R] : Group (Tropical R) :=
{ instMonoidTropical with
inv := Inv.inv
div_eq_mul_inv := fun _ _ => untrop_injective <| by simp [sub_eq_add_neg]
inv_mul_cancel := fun _ => untrop_injective <| neg_add_cancel _
zpow := fun n x => trop <| n • untrop x
zpow_zero' := fun _ => untrop_injective <| zero_zsmul _
zpow_succ' := fun _ _ => untrop_injective <| SubNegMonoid.zsmul_succ' _ _
zpow_neg' := fun _ _ => untrop_injective <| SubNegMonoid.zsmul_neg' _ _ }
