Theorems · Inductive type · ring theory

StarAlgHom

(R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [Algebra R A] → [Star A] → [inst_4 : Semiring B] → [Algebra R B] → [Star B] → Type (max u_2 u_3)

A ⋆-algebra homomorphism is an algebra homomorphism between 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

215 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraStarSemiringAlgebraStar