refl

Mathlib.Algebra.AddConstMap.Equiv

URI: https://scilib.ai/kg/mathlib#AddConstEquiv.refl

Lean4

/-- The identity map as an `AddConstEquiv`. -/
@[simps! toEquiv apply]
def refl (a : G) : G ≃+c[a, a] G where
  toEquiv := .refl G
  map_add_const' _ := rfl

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

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

Разделы

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

Аффилиация

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