English
For any ring R, the map algebraMap from ℤ to R is definitionally equal to Int.castRingHom R; i.e., the two natural integer embeddings coincide.
Русский
Для любого кольца R отображение algebraMap ℤ R совпадает с Int.castRingHom R; то есть две естественные встроенные целочисленные вложения совпадают.
LaTeX
$$$\mathrm{algebraMap}_{\mathbb{Z}} R = \mathrm{Int.castRingHom} R$.$$
Lean4
/-- A special case of `eq_intCast'` that happens to be true definitionally -/
@[simp]
theorem algebraMap_int_eq : algebraMap ℤ R = Int.castRingHom R :=
rfl