unzero_mul — Mathlib

English

If x,y are WithZero α and x*y ≠ 0, then unzero(x*y) = unzero(left) * unzero(right) where left and right are the zero-unzero components of x and y.

Русский

Пусть x,y — элементы WithZero α и x*y ≠ 0. Тогда unzero(x*y) = unzero(left) · unzero(right).

LaTeX

$$For hxy ≠ 0, unzero(hxy) = unzero(left_of_mul hxy) * unzero(right_of_mul hxy)$$

Lean4

theorem unzero_mul {x y : WithZero α} (hxy : x * y ≠ 0) :
    unzero hxy = unzero (left_ne_zero_of_mul hxy) * unzero (right_ne_zero_of_mul hxy) := by
  simp only [← coe_inj, coe_mul, coe_unzero]

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