toRingEquiv_toRingHom

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.toRingEquiv_toRingHom

English

There is a canonical coercion from AlgEquiv to ring equivalences.

Русский

Существует каноническое приведение AlgEquiv к кольцевым эквивалентностям.

LaTeX

$$$\\text{coe\_ringEquiv} : \\text{AlgEquiv} \\to (\\text{A} \\simeq_\\mathrm{+}^* \\text{B})$$$

Lean4

@[simp, norm_cast]
theorem toRingEquiv_toRingHom : ((e : A₁ ≃+* A₂) : A₁ →+* A₂) = e :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru