English
Let A and B be (not necessarily unital) semirings equipped with a star operation. If F is a collection of maps from A to B that is compatible with an EquivLike structure between A and B and also forms a RingEquivClass and a StarRingEquivClass, then F constitutes a class of nonunital star-ring homomorphisms from A to B.
Русский
Пусть A и B — полугруппы типа полусложного кольца со звездой (не обязательно с единицей). Если F является множеством отображений A → B, совместимым с эквивалентностью между A и B и образует структуры RingEquivClass и StarRingEquivClass, то F образует класс немонодированных гомоморфизмов звёздного кольца из A в B.
LaTeX
$$$\\text{NonUnitalStarRingHomClass}(F,A,B)$$$
Lean4
instance (priority := 100) {F A B : Type*} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B]
[EquivLike F A B] [RingEquivClass F A B] [StarRingEquivClass F A B] : NonUnitalStarRingHomClass F A B :=
{ }
