Theorems · Theorem · ring theory

StarAlgEquiv.toStarAlgHom_comp

∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  [inst_7 : Star A₁] [inst_8 : Star A₂] [inst_9 : Star A₃] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₂ : A₂ ≃⋆ₐ[R] A₃),
  e₂.toStarAlgHom.comp e₁.toStarAlgHom = (e₁.trans e₂).toStarAlgHom

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

0 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebraStarStarStar