Theorems · Theorem · order theory

WithTop.mul_def

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : WithTop α),
  a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (fun x1 x2 => x1 * x2) a b

Defined in

Mathlib.Algebra.Order.Ring.WithTop

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

DecidableEqMulZeroClass