toRingHom_toOpposite — Mathlib

English

The toRingHom of an opposite algebra hom equals the opposite of the RingHom.

Русский

toRingHom противоположного алгебра-гомоморфизма равен противоположному RingHom.

LaTeX

$$toRingHom_toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :$$

Lean4

@[simp]
theorem toRingHom_toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
    (f.toOpposite hf : A →+* Bᵐᵒᵖ) = (f : A →+* B).toOpposite hf :=
  rfl

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