English
Let f: A1 ≃ₐ[R] A2 and g: A2 ≃ₐ[R] A3 be algebra isomorphisms over R. Then the linear map underlying their composition equals the composition of the linear maps: (f.trans g).toLinearMap = g.toLinearMap ∘ f.toLinearMap.
Русский
Пусть f: A1 ≃ₐ[R] A2 и g: A2 ≃ₐ[R] A3 — изоморфизмы по R. Тогда линейный отображатель, лежащий в основе их компоновки, равен композиции линейных отображений: (f.trans g).toLinearMap = g.toLinearMap ∘ f.toLinearMap.
LaTeX
$$$ (f : A_1 \\simeq_{R} A_2) (g : A_2 \\simeq_{R} A_3) \\\\Rightarrow (f.trans g).toLinearMap = g.toLinearMap \\circ f.toLinearMap $$$
Lean4
@[simp]
theorem trans_toLinearMap (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :
(f.trans g).toLinearMap = g.toLinearMap.comp f.toLinearMap :=
rfl
