coe_algHom_ofAlgHom — Mathlib

English

The underlying algebra homomorphism of an algebra equivalence equals the given algebra equivalence map when viewed as a homomorphism.

Русский

Пусть дано эквивалентность алгебр; базовая алгебраическая гомоморфная часть совпадает с данным отображением эквивалентности.

LaTeX

$$$\\mathrm{coe\\_algHom\\_ofAlgHom}:\\; \\text{if } f,g,h_1,h_2, \\; \\bigl\\uparrow(\\mathrm{ofAlgHom} f g h_1 h_2) = f$$$

Lean4

theorem coe_algHom_ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : ↑(ofAlgHom f g h₁ h₂) = f :=
  rfl

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