opOp — Mathlib

English

The op of an algebra hom’s ring hom component equals the ring op of the original ring hom.

Русский

Обратимая часть кольцевого отображения сохраняет операцию противоположности.

LaTeX

$$f.op.toRingHom = RingHom.op f.toRingHom$$

Lean4

/-- An algebra is isomorphic to the opposite of its opposite. -/
@[simps!]
def opOp : A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ where
  __ := RingEquiv.opOp A
  commutes' _ := rfl

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