no goals
α : Type ?u.929509
a : ZNum
⊢ ↑(0 * a) = ↑0 * ↑a
cases a <;> exact (MulZeroClass.zero_mul _).symm
no goals
α : Type ?u.929509
b : ZNum
⊢ ↑(b * 0) = ↑b * ↑0
cases b <;> exact (MulZeroClass.mul_zero _).symm
no goals
α : Type ?u.929509
a b : PosNum
⊢ -↑(a * b) = ↑a * -↑b
rw [PosNum.cast_mul, neg_mul_eq_mul_neg]
no goals
α : Type ?u.929509
a b : PosNum
⊢ -↑(a * b) = -↑a * ↑b
rw [PosNum.cast_mul, neg_mul_eq_neg_mul]
no goals
α : Type ?u.929509
a b : PosNum
⊢ ↑(a * b) = -↑a * -↑b
rw [PosNum.cast_mul, neg_mul_neg]