Theorems · Inductive type · ring theory

NonUnitalStarAlgHom

(R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [DistribMulAction R A] →
            [Star A] → [inst_4 : NonUnitalNonAssocSemiring B] → [DistribMulAction R B] → [Star B] → Type (max u_2 u_3)

A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between non-unital R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

208 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 9 definitions · uses no axioms

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulActionStarNonUnitalNonAssocSemiringDistribMulActionStar