Theorems · Inductive type · ring theory

NonUnitalStarRingHom

(A : Type u_1) →
  (B : Type u_2) →
    [NonUnitalNonAssocSemiring A] → [Star A] → [NonUnitalNonAssocSemiring B] → [Star B] → Type (max u_1 u_2)

A non-unital ⋆-ring homomorphism is a non-unital ring homomorphism between non-unital non-associative semirings A and B equipped with a star operation, and this homomorphism is also star-preserving.

Defined in

Mathlib.Algebra.Star.StarRingHom

Cited by

32 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringStarNonUnitalNonAssocSemiringStar