mul_def — Mathlib

English

The multiplication on WithTop is defined by: a ⋅ b equals 0 if a = 0 or b = 0, otherwise it is the pointwise product.

Русский

Умножение на WithTop задается как: a·b = 0, если a = 0 или b = 0, иначе — произведение значений.

LaTeX

$$$a \\cdot b = \\begin{cases}0, & a = 0 \\lor b = 0 \\\\ map\\₂ (\\cdot)\\ a\\ b, & \\text{иначе} \\end{cases}$$$

Lean4

theorem mul_def (a b : WithTop α) : a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (· * ·) a b := by
  cases a <;> cases b <;> aesop

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