coeRingHom — Mathlib

English

The coercion from the nonnegative subtype to α extends to a ring hom, preserving addition, multiplication, zero, and one.

Русский

Приведение из подтипа неотрицательных элементов в α расширяется до кольцо-гомоморфа, сохраняющего сумму, произведение, ноль и единицу.

LaTeX

$$$ \text{coeRingHom} : { x : \alpha // 0 \le x } \to+* \alpha $ is a RingHom;\n\; (a,b) \mapsto a + b, a b, 0, 1$$

Lean4

/-- Coercion `{x : α // 0 ≤ x} → α` as a `RingHom`. -/
def coeRingHom : { x : α // 0 ≤ x } →+* α :=
  { toFun := ((↑) : { x : α // 0 ≤ x } → α)
    map_one' := Nonneg.coe_one
    map_mul' := Nonneg.coe_mul
    map_zero' := Nonneg.coe_zero, map_add' := Nonneg.coe_add }

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