algebraMap_comp_intCast — Mathlib

English

Let R be a commutative ring and A a ring, with A an R-algebra. Then algebraMap R A ∘ Int.cast = Int.cast holds, i.e., the integer embedding into A is compatible with the embedding of ℤ into R.

Русский

Пусть R — коммутативное кольцо, A — кольцо, и A — R-алгебра. Тогда выполняется равенство algebraMap R A ∘ Int.cast = Int.cast, то есть вложение целых в A согласуется с вложением целых в R.

LaTeX

$$$\mathrm{algebraMap}\; R\; A \circ \mathrm{Int.cast} = \mathrm{Int.cast}.$$$

Lean4

@[simp]
theorem algebraMap_comp_intCast (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
    algebraMap R A ∘ Int.cast = Int.cast := by ext; simp

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