triples — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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