toAlgEquiv_toRingHom — Mathlib

English

Let e: A ≃ₐc[R] B. Then the underlying ring homomorphism of the AlgEquiv part coincides with the ring homomorphism associated to e.

Русский

Пусть e: A ≃ₐc[R] B. Тогда подлежащий кольцевой гомоморфизм части AlgEquiv совпадает с кольцевым гомоморфизмом, соответствующим e.

LaTeX

$$$((e : A \\equiv_{\\mathcal{A}R} B) : A \\to_{+*} B) = e$$$

Lean4

@[simp]
theorem toAlgEquiv_toRingHom (e : A ≃ₐc[R] B) : ((e : A ≃ₐ[R] B) : A →+* B) = e :=
  rfl

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