triples₂ — Mathlib

English

If σ12: R1 → R2 and σ21: R2 → R1 form an inverse pair, then the triple RingHomCompTriple σ21 σ12 (RingHom.id R2) holds, i.e. σ12 ∘ σ21 = id_{R2}.

Русский

Если σ12: R1 → R2 и σ21: R2 → R1 образуют обратную пару, то тройка RingHomCompTriple σ21 σ12 (RingHom.id R2) выполняется, то есть σ12 ∘ σ21 = id_{R2}.

LaTeX

$$$\sigma_{12} \circ \sigma_{21} = \mathrm{id}_{R_2}$$$

Lean4

instance triples₂ {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] : RingHomCompTriple σ₂₁ σ₁₂ (RingHom.id R₂) :=
  ⟨by simp only [comp_eq₂]⟩

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