coeAddMonoidHom — Mathlib

English

The coercion map from the nonnegative subtype to the ambient type is an additive monoid hom, preserving zero and addition.

Русский

Переход из подтипа неотрицательных элементов в внешний тип сохраняет ноль и аддитивное сложение.

LaTeX

$$$ \text{coeAddMonoidHom} : \{ x : \alpha // 0 \le x \} \to+\!\alpha $ is an additive monoid hom;\n\; (a,b) \mapsto a + b$$

Lean4

/-- Coercion `{x : α // 0 ≤ x} → α` as an `AddMonoidHom`. -/
@[simps]
def coeAddMonoidHom : { x : α // 0 ≤ x } →+ α :=
  { toFun := ((↑) : { x : α // 0 ≤ x } → α)
    map_zero' := Nonneg.coe_zero
    map_add' := Nonneg.coe_add }

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