coe_castAddMonoidHom — Mathlib

English

The underlying function of castAddMonoidHom coincides with the standard nat-to-α embedding.

Русский

Функция castAddMonoidHom совпадает с каноничным вложением чисел Натуральных в α.

LaTeX

$$$ (castAddMonoidHom\, \alpha) : \mathbb{N} \to \alpha \text{ acts as } n \mapsto \operatorname{Nat.cast}(n).$$$

Lean4

@[simp]
theorem coe_castAddMonoidHom [AddMonoidWithOne α] : (castAddMonoidHom α : ℕ → α) = Nat.cast :=
  rfl

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