English
The natural embedding of integers into any nonunital ring preserves multiplication: for all m,n ∈ ℤ and any NonAssocRing α, ((m·n) : α) = (m : α) · (n : α).
Русский
Естественное вложение целых чисел в произвольное немонопольное кольцо сохраняет умножение: для всех m,n ∈ ℤ и α, ((m·n):α) = (m:α)·(n:α).
LaTeX
$$$\forall \alpha\; [\text{NonAssocRing } \alpha],\; \forall m,n:\mathbb{Z},\; ((m\cdot n) : \alpha) = (m : \alpha) \cdot (n : \alpha)$$$
Lean4
@[simp, norm_cast]
theorem cast_mul {α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fun m =>
by
obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m
·
induction m with
| zero => simp
| succ m ih => simp_all [add_mul]
·
induction m with
| zero => simp
| succ m ih => simp_all [add_mul]
