English
Let e1:e2:e3 and e1':e2' be algebra isomorphisms and e2,e2' as above; then transporting with a composition respects composition: arrowCongr (e1.trans e2) (e1'.trans e2') = (arrowCongr e1 e1').trans (arrowCongr e2 e2').
Русский
Пусть есть последовательность изоморфизмов, и перенос через композицию сохраняет композицию переносов: arrowCongr (e1.trans e2) (e1'.trans e2') = (arrowCongr e1 e1').trans (arrowCongr e2 e2').
LaTeX
$$$\\forall {e_1,e_1',e_2,e_2'}\\,\\text{ with appropriate types },\\ arrowCongr (e_1.trans e_2) (e_1'.trans e_2') = (arrowCongr e_1 e_1').trans (arrowCongr e_2 e_2').$$$
Lean4
@[simp]
theorem arrowCongr_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂') (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃') :
arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂') :=
rfl
