untopD_zero_mul — Mathlib

English

For any a,b in WithTop, (a⋅b).untopD 0 = a.untopD 0 ⋅ b.untopD 0.

Русский

Для любых a,b из WithTop: (a⋅b).untopD 0 = a.untopD 0 ⋅ b.untopD 0.

LaTeX

$$$\\forall a,b \\in WithTop(\\alpha),\\ (a \\cdot b).untopD 0 = a.untopD 0 \\cdot b.untopD 0$$$

Lean4

@[simp]
theorem untopD_zero_mul (a b : WithTop α) : (a * b).untopD 0 = a.untopD 0 * b.untopD 0 :=
  by
  by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
  by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
  cases a; · rw [top_mul hb, untopD_top, zero_mul]
  cases b; · rw [mul_top ha, untopD_top, mul_zero]
  rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]

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