coe_trans — Mathlib

English

The underlying function of the trans composition equals the composition of the underlying functions: the functorial action matches.

Русский

Функция–порожденная композиция совпадает с композицией функций.

LaTeX

$$$\bigl\langle e_1 \bigr\rangle_{A_1,A_2} \circ \bigl\langle e_2 \bigr\rangle_{A_2,A_3} = \bigl\langle e_2 \bigr\rangle_{A_2,A_3} \circ \bigl\langle e_1 \bigr\rangle_{A_1,A_2}$$$

Lean4

@[simp]
theorem coe_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ :=
  rfl

Похожие утверждения