toRingHomClass — Mathlib

English

From a RingEquivClass, one obtains a RingHomClass between the two rings, preserving zero and one.

Русский

Из RingEquivClass получают RingHomClass между двумя кольцами, сохраняющий нуль и единицу.

LaTeX

$$RingHomClass F R S$$

Lean4

instance (priority := 100) toRingHomClass [NonAssocSemiring R] [NonAssocSemiring S] [h : RingEquivClass F R S] :
    RingHomClass F R S :=
  { h with
    map_zero := map_zero
    map_one := map_one }
    -- See note [lower instance priority]

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