algebraMap_eq_inlRingHom

Mathlib.Algebra.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.algebraMap_eq_inlRingHom

English

Equality of elements in Unitization is testable by their fst and snd components.

Русский

Равенство элементов Unitization можно проверить по их компонентам fst и snd.

LaTeX

$$$x = y \Leftrightarrow x.1 = y.1 \text{ and } x.2 = y.2$$$

Lean4

theorem algebraMap_eq_inlRingHom : algebraMap R (Unitization R A) = inlRingHom R A :=
  rfl

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

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

Разделы

Аффилиация

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