English
Let α be a type with a zero and a multiplication. For any a,b ∈ WithBot α, the product a ∘ b equals 0 if either a or b is 0; otherwise a ∘ b corresponds to the product of the underlying α-values. In other words, the multiplication on the bottom-extended type is given by 0 if either factor is 0, and otherwise is the lift of the usual product from α.
Русский
Пусть α — множество с нулём и умножением. Для любых a, b ∈ WithBot α произведение a · b равно 0, если хотя бы одно из чисел равно 0; в противном случае произведение соответствует произведению соответствующих элементов в α (то есть если a = some x и b = some y, то a · b = some (x · y)).
LaTeX
$$$ a*b = \begin{cases} \bot, & a = \bot \\ \text{some }(x y), & a = \text{some } x \text{ and } b = \text{some } y \ \end{cases} $$$
Lean4
theorem mul_def (a b : WithBot α) : a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (· * ·) a b := by
cases a <;> cases b <;> aesop
