algebraMap_comp_natCast — Mathlib

English

For any commutative semiring R, any semiring A, and any Algebra structure on A over R, the precomposition of algebraMap with the natural casting from ℕ to R equals the natural casting to A: algebraMap R A ∘ Nat.cast = Nat.cast.

Русский

Для любой коммутативной полупрямой кольцевой структуры R, любого полупрямого кольца A и алгебровой структуры A над R, композиция algebraMap R A с Nat.cast совпадает с Nat.cast в A.

LaTeX

$$$\mathrm{algebraMap}_R A \circ \mathrm{Nat.cast} = \mathrm{Nat.cast}$. $$

Lean4

@[simp]
theorem algebraMap_comp_natCast (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
    algebraMap R A ∘ Nat.cast = Nat.cast := by ext; simp

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