algebraMap_toAlgebra'

Mathlib.Algebra.Algebra.Defs

URI: https://scilib.ai/kg/mathlib#RingHom.algebraMap_toAlgebra'

← MathLib Explorer

English

The algebraMap obtained from RingHom toAlgebra' equals the original RingHom i.

Русский

Алгебраическая карта, полученная через RingHom.toAlgebra', равна исходному RingHom i.

LaTeX

$$$\text{algebraMap } R S^{toAlgebra'} = i$.$$

Lean4

theorem algebraMap_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) :
    @algebraMap R S _ _ (i.toAlgebra' h) = i :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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