Theorems · Inductive type · ring theory

NonUnitalStarRingHomClass

(F : Type u_1) →
  (A : outParam (Type u_2)) →
    (B : outParam (Type u_3)) →
      [inst : NonUnitalNonAssocSemiring A] →
        [Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [Star B] → [inst_4 : FunLike F A B] → [NonUnitalRingHomClass F A B] → Prop

NonUnitalStarRingHomClass F A B states that F is a type of non-unital ⋆-ring homomorphisms. You should also extend this typeclass when you extend NonUnitalStarRingHom.

Defined in

Mathlib.Algebra.Star.StarRingHom

Cited by

5 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringStarNonUnitalNonAssocSemiringStarFunLikeNonUnitalRingHomClass