mapDomain_id

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.mapDomain_id

English

Mapping domain with the identity map leaves SkewMonoidAlgebra unchanged.

Русский

Переобразование области с тождественным отображением не меняет SkewMonoidAlgebra.

LaTeX

$$$$ mapDomain id v = v $$$$

Lean4

theorem mapDomain_id : mapDomain id v = v :=
  sum_single _

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

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

Разделы

Аффилиация

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