apply

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.Simps.apply

English

The apply projection from a nonunital algebra homomorphism to functions simply returns the underlying map f itself.

Русский

Проекция применения из гомоморфизма без единицы к функциям просто возвращает сам отображение f как функцию.

LaTeX

$$$\text{apply}(f) = f$$$

Lean4

/-- See Note [custom simps projection] -/
def apply (f : A →ₛₙₐ[φ] B) : A → B :=
  f

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

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

Разделы

Аффилиация

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