algebraMap_int_eq — Mathlib

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

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