mul_eq_zero_iff — Mathlib

English

There is an instance asserting no zero divisors for Tropical (WithTop R).

Русский

Существует экземпляр, утверждающий отсутствие нулевых делителей в Tropical(WithTop R).

LaTeX

$$$\mathrm{NoZeroDivisors} (\mathrm{Tropical}(\mathrm{WithTop}(R)))$$$

Lean4

theorem mul_eq_zero_iff {R : Type*} [AddCommMonoid R] {a b : Tropical (WithTop R)} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
  simp [← untrop_inj_iff, WithTop.add_eq_top]

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