English
Let π(a) = a.unbotD 0 ∈ α. Then π respects multiplication: π(a*b) = π(a) · π(b). More explicitly, the underlying map to α preserves the product under multiplication.
Русский
Пусть π(a) = a.unbotD 0 ∈ α. Тогда π сохраняет умножение: π(a*b) = π(a) · π(b).
LaTeX
$$$ (a*b).unbotD 0 = a.unbotD 0 \cdot b.unbotD 0 $$$
Lean4
@[simp]
theorem unbotD_zero_mul (a b : WithBot α) : (a * b).unbotD 0 = a.unbotD 0 * b.unbotD 0 :=
by
by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]
cases a; · rw [bot_mul hb, unbotD_bot, zero_mul]
cases b; · rw [mul_bot ha, unbotD_bot, mul_zero]
rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]
