instMonoidTropical — Mathlib

English

Tropical R carries a Monoid structure whenever R is an AddMonoid.

Русский

Tropical R образует моноид, если R является аддитивным моноидом.

LaTeX

$$$\\operatorname{Monoid}(\\operatorname{Tropical}(R))$$$

Lean4

instance instMonoidTropical [AddMonoid R] : Monoid (Tropical R) :=
  { instMulOneClassTropical,
    instSemigroupTropical with
    npow := fun n x => x ^ n
    npow_zero := fun _ => untrop_injective <| by simp
    npow_succ := fun _ _ => untrop_injective <| succ_nsmul _ _ }

Похожие утверждения