English
Let R and S be rings and let e: R ≃+* S be a ring isomorphism. Suppose e' : S → R and h1, h2 witness that e' is a two-sided inverse of the underlying equivalence, and h3, h4 express that e' respects multiplication and addition via e. Then the ring isomorphism constructed from this data coincides with e; i.e. the canonical construction yields the original isomorphism.
Русский
Пусть R и S — кольца, и e: R ≃+* S — кольцевой изоморфизм. Предположим, что e' : S → R и доказательства h1, h2 показывают, что e' является двухсторонним обратным к соответствующей эквиваленции, а h3, h4 устанавливают сохранение умножения и сложения при использовании e'. Тогда кольцевой изоморфизм, построенный из этих данных, совпадает с e; т.е. стандартная конструкция возвращает исходный изоморфизм.
LaTeX
$$$\\left( \\langle \\langle e, e', h_1, h_2 \\rangle, h_3, h_4 \\rangle : R \\cong_+* S \\right) = e$$$
Lean4
@[simp]
theorem mk_coe (e : R ≃+* S) (e' h₁ h₂ h₃ h₄) : (⟨⟨e, e', h₁, h₂⟩, h₃, h₄⟩ : R ≃+* S) = e :=
ext fun _ => rfl
