toRingEquiv_toOpposite — Mathlib

English

The ring equivalence coming from the opposite construction coincides with the standard opposite ring equivalence.

Русский

Кольцевое эктививелентное построение, получаемое через противоположность, совпадает со стандартным RingEquiv.toOpposite.

LaTeX

$$$ (toOpposite\\,R\\,A : A \\to (A)^{op}) = RingEquiv.toOpposite A $$$

Lean4

@[simp]
theorem toRingEquiv_toOpposite : (toOpposite R A : A ≃+* Aᵐᵒᵖ) = RingEquiv.toOpposite A :=
  rfl

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