apply — Mathlib

English

There is a custom projection for simps so that applying an AlgHom via Simps yields its usual action on inputs.

Русский

У AlgHom.Simps существует особая проекция для simp, так что применение через Simps даёт обычное действие на аргументах.

LaTeX

$$$\\text{AlgHom.Simps}.apply(f) = f$$$

Lean4

/-- See Note [custom simps projection] -/
def apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β]
    (f : α →ₐ[R] β) : α → β :=
  f

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