coe

Mathlib.Algebra.Star.MonoidHom

URI: https://scilib.ai/kg/mathlib#StarMonoidHom.Simps.coe

English

The Simps projection coe picks out the underlying function of a StarMonoidHom.

Русский

Проекция coe выбирает базовую функцию StarMonoidHom.

LaTeX

$$coe (f : A \rightarrow⋆* B) : A → B := f$$

Lean4

/-- See Note [custom simps projection] -/
def coe (f : A →⋆* B) : A → B :=
  f

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

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

Разделы

Аффилиация

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