toRingEquiv_toRingHom — Mathlib

English

If e is a bialg equivalence A ≃ₐc[R] B, then the underlying ring homomorphism extracted from e agrees with the same map regarded as a ring homomorphism from the underlying ring isomorphism.

Русский

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

LaTeX

$$$((e : A \\simeq_ {+*} B) : A \\to_{+*} B) = e$$$

Lean4

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

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