mapRangeRingHom_id

Mathlib.Algebra.MonoidAlgebra.Lift

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.mapRangeRingHom_id

English

The mapRangeRingHom with the identity ring hom is the identity on the monoid algebra: mapRangeRingHom M id_R = id_(R[M]).

Русский

MapRangeRingHom с тождественным гомоморфизмом даёт тождественный отображение на R[M].

LaTeX

$$$ mapRangeRingHom\ M\ id_R = id\ (R[M]) $$$

Lean4

@[simp]
theorem mapRangeRingHom_id : mapRangeRingHom M (.id R) = .id (R[M]) := by ext <;> simp

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

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

Разделы

Аффилиация

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