symm — Mathlib

English

Swapping the directions of an inverse pair yields another inverse pair.

Русский

Поменяв направления в обратной паре, получаем другую обратную пару.

LaTeX

$$RingHomInvPair σ₂₁ σ₁₂$$

Lean4

/-- Swap the direction of a `RingHomInvPair`. This is not an instance as it would loop, and better
instances are often available and may often be preferable to using this one. Indeed, this
declaration is not currently used in mathlib.
-/
theorem symm (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁) [RingHomInvPair σ₁₂ σ₂₁] : RingHomInvPair σ₂₁ σ₁₂ :=
  ⟨RingHomInvPair.comp_eq₂, RingHomInvPair.comp_eq⟩

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