add_pow — Mathlib

English

In Tropical (WithTop R) with AddCommMonoid R, there are no zero divisors: if a*b = 0, then a = 0 or b = 0.

Русский

В Tropical(WithTop R) при AddCommMonoid R нулевых делителей нет: если a·b = 0, то a = 0 или b = 0.

LaTeX

$$$\forall a,b \in \mathrm{Tropical}(\mathrm{WithTop}(R)),\ a\cdot b = 0 \Rightarrow a = 0 \lor b = 0$$$

Lean4

@[simp]
theorem add_pow [LinearOrder R] [AddMonoid R] [AddLeftMono R] [AddRightMono R] (x y : Tropical R) (n : ℕ) :
    (x + y) ^ n = x ^ n + y ^ n := by
  rcases le_total x y with h | h
  · rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]
  · rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]

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