coeMonoidHom — Mathlib

English

The coercion map extends to a MonoidHom from ℕ+ to ℕ, i.e., it preserves both multiplication and identity.

Русский

Преобразование расширяется до моноид-гомоморфа: ℕ+ → ℕ, сохраняющего умножение и единицу.

LaTeX

$$$ \\mathrm{coeMonoidHom}: \\mathbb{N}^+ \\to^* \\mathbb{N} \\quad\\text{with}\\quad \\mathrm{toFun}=\\text{coe},\\; \\mathrm{map_one'}=\\text{one_coe},\\; \\mathrm{map_mul'}=\\text{mul_coe}. $$$

Lean4

/-- `PNat.coe` promoted to a `MonoidHom`. -/
def coeMonoidHom : ℕ+ →* ℕ where
  toFun := Coe.coe
  map_one' := one_coe
  map_mul' := mul_coe

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