Theorems · Theorem · ring theory

StarAlgEquiv.arrowCongr_comp

∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  [inst_13 : Star A₁] [inst_14 : Star A₂] [inst_15 : Star A₃] [inst_16 : Star A₁'] [inst_17 : Star A₂']
  [inst_18 : Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₐ[R] A₂)
  (g : A₂ →⋆ₐ[R] A₃), (e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraStarStarStarStarStarStar