mapDomainBialgHom_id

Mathlib.RingTheory.Bialgebra.MonoidAlgebra

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

English

The mapDomainBialgHom respects identity on M: mapDomainBialgHom R (.id M) = .id _ _.

Русский

mapDomainBialgHom сохраняет тождественный морфизм на M: mapDomainBialgHom R (id M) = id.

LaTeX

$$$mapDomainBialgHom\ R\ (\mathrm{id}\ M) = \mathrm{id}\ R\ (M)$$$

Lean4

@[simp]
theorem mapDomainBialgHom_id : mapDomainBialgHom R (.id M) = .id _ _ := by ext; simp

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

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

Разделы

Аффилиация

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