apply

Mathlib.Algebra.Algebra.Equiv

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

English

The Simps projection for an algebra equivalence is the function part of the equivalence.

Русский

Проекция Simps для алгебровой эквивалентности совпадает с функцией эквивалентности.

LaTeX

$$$\text{Simps.apply}(e) = e$$$

Lean4

/-- See Note [custom simps projection] -/
def apply (e : A₁ ≃ₐ[R] A₂) : A₁ → A₂ :=
  e

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

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

Разделы

Аффилиация

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