ofAlgHom_symm — Mathlib

English

If f:A1→ₐ[R]A2 and g:A2→ₐ[R]A1 satisfy the inverse equations, then the opposite algebra equivalence has flipped maps as its forward and inverse.

Русский

Если есть пары симметричных алгебраических отображений с взаимно обратными свойствами, получаем обратную алгебраическую эквивалентность.

LaTeX

$$$\\mathrm{(ofAlgHom\\;f\\;g\\;h_1\\;h_2).symm = ofAlgHom\\;g\\;f\\;h_2\\;h_1}$$$

Lean4

theorem ofAlgHom_symm (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : (ofAlgHom f g h₁ h₂).symm = ofAlgHom g f h₂ h₁ :=
  rfl

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