English
For all m,n in ZNum, the image in ℤ of their product equals the product of their images in ℤ.
Русский
Для любых m,n ∈ ZNum образ их произведения в ℤ равен произведению образов в ℤ.
LaTeX
$$$$\forall m,n \in ZNum,\ ((m * n : ZNum) : ℤ) = (m : ℤ) \cdot (n : ℤ).$$$$
Lean4
@[simp, norm_cast]
theorem mul_to_int : ∀ m n, ((m * n : ZNum) : ℤ) = m * n
| 0, a => by cases a <;> exact (zero_mul _).symm
| b, 0 => by cases b <;> exact (mul_zero _).symm
| pos a, pos b => PosNum.cast_mul a b
| pos a, neg b => show -↑(a * b) = ↑a * -↑b by rw [PosNum.cast_mul, neg_mul_eq_mul_neg]
| neg a, pos b => show -↑(a * b) = -↑a * ↑b by rw [PosNum.cast_mul, neg_mul_eq_neg_mul]
| neg a, neg b => show ↑(a * b) = -↑a * -↑b by rw [PosNum.cast_mul, neg_mul_neg]
